proposition: Lemma nat_dist_less_than_one_iff_equal : forall n m : ℕ, (n = m) <-> (| m - n | < 1).
proof: Proof. Take n, m : nat. We show both directions. - We need to show that (n = m ⇨ |m - n| < 1). Assume that (n = m). We argue by contradiction. Assume that (~ | m - n | < 1). It holds that (1 <= | m - n|). It holds that (~(n=m)). Contradiction. - We need to show that (| m - n | < 1 -> n = m). Assume that (| m - n| < 1). We argue by contradiction. Assume that (~ (n = m)). It holds that (1 <= | m - n|). Contradiction. Qed.
imports: Coq.Reals.Reals Tactics Automation Libs.Negation Notations