proposition: Lemma lt_lt_succ n m : n < m -> n < succ m.
proof: Proof. intros. now apply lt_succ_r, lt_le_incl. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef