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