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