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