proposition: Lemma nexp_funny : forall x y : R, (x[+]y) [*] (x[-]y) [=] x[^]2[-]y[^]2.
proof: Proof. intros x y. astepl (x[*] (x[-]y) [+]y[*] (x[-]y)). astepl (x[*]x[-]x[*]y[+] (y[*]x[-]y[*]y)). astepl (x[*]x[+] [--] (x[*]y) [+] (y[*]x[+] [--] (y[*]y))). astepl (x[*]x[+] [--] (x[*]y) [+]y[*]x[+] [--] (y[*]y)). astepl (x[*]x[+] ( [--] (x[*]y) [+]y[*]x) [+] [--] (y[*]y)). astepl (x[*]x[+] ( [--] (x[*]y) [+]x[*]y) [+] [--] (y[*]y)). astepl (x[*]x[+][0][+] [--] (y[*]y)). astepl (x[*]x[+] [--] (y[*]y)). Step_final (x[*]x[-]y[*]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)