proposition: Lemma add_carry_reg_l p q r : add_carry p q = add_carry p r -> q = r.
proof: Proof. intros H; apply (add_reg_r _ _ p); rewrite (add_comm r), (add_comm q); now apply add_carry_add. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef