proposition: Theorem lt_le_incl : ∀ n m, n < m → n ≤ m.
proof: Proof. intros n m H. destruct n as [n| ]; [ idtac | inversion H ]. destruct m as [m| ]; [ idtac | constructor ]. constructor; apply Nat.lt_le_incl; inversion H; assumption. Qed.
imports: Utf8 Compare_dec NPeano Misc