proposition: Remark add_sub_square_identity : forall a b : nat, (b + a - b) * (b + a - b) = (b + a) * (b + a) + b * b - 2 * ((b + a) * b).
proof: Proof. intros a b; rewrite (Nat.add_comm b a) at 1 2; rewrite Nat.add_sub. repeat rewrite Nat.mul_add_distr_r || rewrite <- (Nat.mul_comm (b + a)). replace (b * b + a * b + (b * a + a * a) + b * b) with (b * b + a * b + (b * b + a * b + a * a)); try (ring; fail). rewrite expand_mult2; repeat rewrite Nat.add_sub; auto with *. Qed.
imports: Coq(ArithRing) Coq(Compare_dec) Coq(Wf_nat) Coq(Arith) Coq(Lia)