Jon, 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[]); Roger _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
