proposition: Lemma eq_mult : forall a b c : nat, c <> 0 -> c * a = c * b -> a = b.
proof: Proof. intros a b c; case c; auto. intros H'; case H'; auto. intros n H' H'0; apply simpl_mult_r with (n := S n); repeat rewrite Nat.mul_comm with (m := S n); auto with arith. Qed.
imports: Coq(Arith ArithRing)