proposition: Lemma succ_lt_mono n m : n < m <-> succ n < succ m.
proof: Proof. unfold lt. now rewrite compare_succ_succ. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef