please how I can use add_comm for transform n<=m <-> n+ p <=m+p into n<=m <-> p+n <=p+m

Maybe something like `rewrite !Nat.add_comm`

if I understand you

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.

whoops, of course

Last updated: Jun 23 2024 at 05:02 UTC