proposition: Lemma nat_not_equal_dist_larger_one : for all n m : ℕ, (n ≠ m) -> (1 ≤ | m - n |).
proof: Proof. Take n, m : ℕ. Assume that (n ≠ m). assert (n > m ∨ n < m)%nat as i by (apply Nat.lt_gt_cases; auto). Because (i) either (n > m)%nat or (n < m)%nat holds. + Case (n > m)%nat. It holds that (| n - m | = | m - n | ). It holds that (1 <= | n - m |). We conclude that (1 <= | m - n |). + Case (m > n)%nat. We conclude that (1 <= | m - n |). Qed.
imports: Coq.Reals.Reals Tactics Automation Libs.Negation Notations