Rob, Thank you. Just one more question: and how about floating numbers? How to prove it?
For example: set_merge_pcs["'z_reals", "z_library"]; set_goal([], %SZT% 0.4 %mem% 0.1 ..%down%R 1.9 %>%); a(rewrite_tac[z_%bbR%_dot_dot_def]); With those steps, ProofPower change the goal to: %SZT%0.1 %leq%%down%R 0.4 %and% 0.4 %leq%%down%R 1.9%>% How can I prove it? Thanks again. Regards, -- Artur Oliveira Gomes
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
