Require Export Coq.Reals.RIneq.
Require Export Coq.Reals.R_sqrt.
Require Export Coq.Reals.Rpower.

Local Open Scope Z_scope.
Local Open Scope R_scope.

About Rplus_eq_reg_l.

Example test: forall a b:R, Rsqr (a + b) = Rsqr a + 2*a*b + Rsqr b.
Proof. intros.
  unfold Rsqr.
  rewrite Rmult_plus_distr_r.
  rewrite Rmult_plus_distr_l.
  rewrite Rmult_plus_distr_l.
  rewrite <- Rplus_assoc.