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