proposition: Lemma double_succ p : (succ p)~0 = succ (succ p~0).
proof: Proof. now destruct p. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef