proposition: Theorem add_assoc p q r : p + (q + r) = p + q + r.
proof: Proof. revert q r. induction p. - intros [q|q| ] [r|r| ]; simpl; f_equal; trivial; rewrite ?add_carry_spec, ?add_succ_r, ?add_succ_l, ?add_1_r; f_equal; trivial. - intros [q|q| ] [r|r| ]; simpl; f_equal; trivial; rewrite ?add_carry_spec, ?add_succ_r, ?add_succ_l, ?add_1_r; f_equal; trivial. - intros q r; rewrite 2 add_1_l, add_succ_l; auto. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef