proposition: Lemma add_xI_pred_double p q : (p + q)~0 = p~1 + pred_double q.
proof: Proof. change (p~1) with (p~0 + 1). now rewrite <- add_assoc, add_1_l, succ_pred_double. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef