proposition: Proposition diseq_implies_lt (n m : nat) : n <> m -> sum (n < m) (n > m).
proof: Proof. intros diseq. destruct (dec (n < m)) as [| a]; [ now left |]. right. destruct (@leq_dichot n m) as [n_leq_m | gt]; [ | assumption]. destruct n_leq_m; [ now contradiction diseq | contradiction a; now apply leq_S_n']. Defined.
imports: Basics Spaces.Nat.Core