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