proposition: Lemma le_lt_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