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