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