proposition: Lemma succ_of_nat (n:nat) : n<>O -> succ (of_nat n) = of_succ_nat n.
proof: Proof. rewrite of_nat_succ. destruct n; trivial. now destruct 1. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef