I should have mentioned that the problem goal you are 
looking at can be solved by linear arithmetic so you don't 
need any lemma at all.
Linear arithmetic is not covered by the tutorlal but this is 
one way to prove the goal:

a (PC_T1 "z_lin_arith" asm_prove_tac[]);


Proofpower mailing list

Reply via email to