proposition: Lemma square_odd_mod4 n: odd n -> n^2 = 1 %[mod 4].
proof: Proof. rewrite -{2} (odd_double_half n) sqrnD => ->. by rewrite mul1n -mul2n mulnA expnMn -addnA -mulnDr addnC mulnC modnMDl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)