The Coq mailing list

[liheng <lihengszh AT gmail.com>]

Hello.
The error occurs when runs  x * x + y * x + (x + y) * y = x * x + 2 * x * y + y * y on rewrite_mult_plus_distr_r。
I don't know the problem and the reasons.
thanks。

code is:
Require Import Arith.
Lemma time2 : forall x y, (x + y) * (x + y) = x*x + 2*x*y + y*y.
Proof.
 intros x y.
 SearchRewrite (_ * (_ + _)).
 rewrite mult_plus_distr_l.
 SearchRewrite ((_ + _) * _).
 rewrite mult_plus_distr_r with (p:=x).
 rewrite_mult_plus_distr_r.
...
Error:
The reference rewrite_mult_plus_distr_r was not found in the current environment.