proposition: Lemma euler's_identity : forall a b c d w x y z : Z, let s z := z * z in (a * a + b * b + c * c + d * d) * (w * w + x * x + y * y + z * z) = s (a*w + b*x + c*y + d*z) + s (a*x - b*w - c*z + d*y) + s (a*y + b*z - c*w - d*x) + s (a*z - b*y + c*x - d*w).
proof: Proof. intros; unfold s. ring. Qed.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm Znumfacts