proposition: Lemma mod4Dsqr_even a b : (a ^ 2 + b ^ 2) %% 4 = 0 -> (~~ odd a) && (~~ odd b).
proof: Proof. have sqr_x2Dy_mod4 x y : (x * 2 + y) ^ 2 = y ^ 2 %[mod 4]. rewrite sqrnD addnAC mulnAC [2 * _]mulnC -mulnA -[2 * 2]/4. by rewrite expnMn -[2 ^ 2]/4 -mulnDl -modnDml modnMl. rewrite {1}(divn_eq a 2) {1}(divn_eq b 2) -modnDm. by rewrite !sqr_x2Dy_mod4 modnDm !modn2; do 2!case: odd. Qed.
imports: mathcomp(all_ssreflect)