proposition: Lemma add_cancel_r p q r : p + r = q + r <-> p = q.
proof: Proof. split. - apply add_reg_r. - congruence. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef