proposition: Lemma lt_le_trans n m p : n < m -> m <= p -> n < p.
proof: Proof. intros H H'. apply le_lteq in H'. destruct H'. - now apply lt_trans with m. - now subst. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef