proposition: Lemma add_reg_l p q r : p + q = p + r -> q = r.
proof: Proof. rewrite 2 (add_comm p). now apply add_reg_r. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef