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