proposition: Lemma _xxx : forall m n, 1 < m -> ~ n < m -> 0 < n.
proof: Proof. destruct n; destruct m; intros. inversion H. exfalso. apply H0. etransitivity. 2: eassumption. repeat constructor. inversion H. now apply Nat.lt_0_succ. Qed.
imports: Coq.Strings.String Coq.Program.Program Coq.Arith.PeanoNat ExtLib.Tactics.Consider ExtLib.Core.RelDec ExtLib.Structures.Reducible ExtLib.Structures.Monoid ExtLib.Data.Char ExtLib.Data.Nat