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