proposition: Lemma lt_trans n m p : n < m -> m < p -> n < p.
proof: Proof. rewrite 3 lt_iff_add. intros (r,Hr) (s,Hs). exists (r+s). now rewrite add_assoc, Hr, Hs. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef