proposition: Theorem add_carry_spec p q : add_carry p q = succ (p + q).
proof: Proof. revert q. induction p; intro q; destruct q; simpl; now f_equal. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef