proposition: Theorem add_succ_l p q : succ p + q = succ (p + q).
proof: Proof. rewrite add_comm, (add_comm p). apply add_succ_r. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef