proposition: Lemma mul_reg_r n m p : p <> 0 -> n * p = m * p -> n = m.
proof: Proof. exact (fun Hp => proj1 (mul_cancel_r n m p Hp)). Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass