proposition: Lemma add_xO_pred_double p q : pred_double (p + q) = p~0 + pred_double q.
proof: Proof. revert q. induction p as [p IHp| p IHp| ]; intro q; destruct q; simpl; rewrite ?add_carry_spec, ?pred_double_succ, ?add_xI_pred_double; try reflexivity. - rewrite IHp; auto. - rewrite <- succ_pred_double, <- add_1_l. reflexivity. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef