lilia Nejoua (Nov 03 2023 at 23:41): lilia Nejoua (Nov 03 2023 at 23:41):please how I can use add_comm for transform n<=m <-> n+ p <=m+p into n<=m <-> p+n <=p+m
Paolo Giarrusso (Nov 04 2023 at 01:04):Maybe something like rewrite !Nat.add_comm if I understand you
Pierre Rousselin (Nov 04 2023 at 15:05):No, please, never use a commutativity lemma with ! (which means as many times as possible) without instantiating at least some of the parameters. This will lead to an infinite loop which may make Coq crash.
Here, something like rewrite 2!(Nat.add_comm _ p). (or rewrite 2!(Nat.add_comm _ p) in H. if your equivalence is an hypothesis, say H, instead of the goal) does the job. The 2! flag means at most twice.
Paolo Giarrusso (Nov 04 2023 at 15:54):whoops, of course
Last updated: Oct 13 2024 at 01:02 UTC