proposition: Theorem mult_reg_l : forall n m p : nat, S n * m = S n * p -> m = p.
proof: Proof. intros n m; elim m; clear m. intros p; case p; simpl in |- *. auto. intros p'; rewrite <- mult_n_O. intros H; discriminate H. intros m' Hrec p; case p. rewrite <- mult_n_O; simpl in |- *; intros H; discriminate H. intros p'; repeat rewrite (Nat.mul_comm (S n)); simpl in |- *. intros H; injection H. intros H'; apply f_equal with (f := S). apply Hrec. repeat rewrite (Nat.mul_comm (S n)). apply Nat.add_cancel_l with n. exact H'. Qed.