proposition: Lemma pred_double_succ p : pred_double (succ p) = p~1.
proof: Proof. induction p; simpl; now f_equal. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef