proposition: Theorem simpl_mult_r : forall n m p : nat, 0 < n -> m * n = p * n -> m = p.
proof: Proof. intros n m; elim m; simpl in |- *; auto. intros p H' H'0; case (mult_eqO p n); auto. intros H'1; Contradict H'; auto; rewrite H'1; auto with arith. intros m' H' p; case p; simpl in |- *; auto. case n; simpl in |- *; try (intros; discriminate); intros H1; Contradict H1; auto with arith. intros p' H'0 H'1. rewrite (H' p'); auto. apply Nat.add_cancel_l with (p := n); auto. Qed.
imports: Coq(Arith ArithRing)