proposition: Lemma nexp_funny' : forall x y : R, (x[-]y) [*] (x[+]y) [=] x[^]2[-]y[^]2.
proof: Proof. intros x y. Step_final ((x[+]y) [*] (x[-]y)). Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CSums CoRN.algebra.CAbMonoids Coq.Sorting.Permutation CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms Coq(Lia)