proposition: Theorem le_lt_trans : ∀ n m p, n ≤ m → m < p → n < p.
proof: Proof. intros n m p Hnm Hmp. destruct p as [p| ]. destruct m as [m| ]; [ simpl | inversion Hmp ]. destruct n as [n| ]; [ simpl | inversion Hnm ]. inversion Hnm; inversion Hmp; constructor. eapply Qle_lt_trans; eassumption. destruct n as [n| ]; [ constructor | idtac ]. inversion Hnm; subst; assumption. Qed.
imports: Utf8 QArith Misc