proposition: Lemma zexp_funny' : forall (x y : R) x_ y_, (x[-]y) [*] (x[+]y) [=] (x[//]x_) [^^] (2) [-] (y[//]y_) [^^] (2).
proof: Proof. intros. astepl ((x[+]y) [*] (x[-]y)). apply zexp_funny. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)