proposition: Lemma lt_S_lt_eq_dec : forall m n, S m < n -> { m < n } + { m = n }.
proof: Proof. intros m n H ; destruct (lt_eq_lt_dec m n) as [[ | ] | ]. left ; assumption. right ; assumption. exfalso ; lia. Qed.
imports: Arith Lia