[isabelle] need help with quantified ints



Hi,
   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,
   Perry

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 MHonArc.