proposition: Lemma le_succ_l n m : succ n <= m <-> n < m.
proof: Proof. rewrite <- lt_succ_r. symmetry. apply succ_lt_mono. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef