proposition: Lemma subR_sqr x y : x ^ 2 - y ^ 2 = (x - y) * (x + y).
proof: Proof. rewrite mulRDr 2!mulRDl -addRA (addRA (- y * x)) (mulRC x y) (addRC _ (y * x)). by rewrite mulNR addRN add0R mulNR addR_opp 2!mulRR. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)