proposition: Theorem sub_square_identity : forall a b : nat, b <= a -> (a - b) * (a - b) = a * a + b * b - 2 * (a * b).
proof: Proof. intros a b H. apply Nat.sub_add in H; rewrite Nat.add_comm in H. rewrite <- H. apply add_sub_square_identity. Qed.
imports: Coq(ArithRing) Coq(Compare_dec) Coq(Wf_nat) Coq(Arith) Coq(Lia)