proposition: Lemma aux1 : for all n m : ℕ, (n = m) ⇒ |m - n| = |n - n|.
proof: Proof. Take n, m : ℕ. Assume that (n = m). We conclude that (& |m - n| = |m - m| = m - m = 0 = n - n = |n - n|). Qed.
imports: Coq.Reals.Reals Tactics Automation Libs.Negation Notations