proposition: Theorem unfold_example : forall x y:Z, x*x = y*y -> Zsquare_diff x y * Zsquare_diff (x+y)(x*y) = 0.
proof: Proof. intros x y Heq. unfold Zsquare_diff at 1. rewrite Heq; ring. Qed.
imports: ZArith List Arith ZArithRing Relations Lia