proposition: Theorem mul_reg_l p q r : r * p = r * q -> p = q.
proof: Proof. rewrite 2 (mul_comm r). apply mul_reg_r. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef