[isabelle] need help with quantified ints
I'm having trouble proving the lemma below. My first idea was to "apply
(cases n)" since there are only 12 values of n that satisfy the assumption,
but that's not possible since n is bound. Also, applying arith, algebra, and
auto have no effect.
Is there any way to make progress?
Thanks in advance,
lemma " !! q qa n. [| 0 < n; int n <= 12; int n * q = 12; int n * qa = 18 |]
==> int n <= 6"
This archive was generated by a fusion of
Pipermail (Mailman edition) and