proposition: Lemma nat_dist_larger_zero_not_equal : forall n m : nat, 0 < | n - m | -> ~(n = m).
proof: Proof. Take n, m : nat. Assume that (0 < | n - m | ). Either (n = m)%nat or (~(n= m))%nat. + Case (n = m)%nat. It holds that (| m - n| = 0). Contradiction. + Case (~(n = m)). We conclude that (~(n = m)). Qed.
imports: Coq.Reals.Reals Tactics Automation Libs.Negation Notations