proposition: Lemma sol_are_even n a b : n > 1 -> sol n a b -> (~~ odd a) && (~~ odd b).
proof: Proof. case: n => [|[|n]]// _; rewrite /sol => /and3P[_ _ /eqP eq_a2Db]. by rewrite mod4Dsqr_even// -eq_a2Db !expnS mulnA modnMr. Qed.
imports: mathcomp(all_ssreflect)