proposition: Lemma pythagore_mod4 x y z: coprime x y -> x ^ 2 + y ^ 2 = z ^ 2 -> odd x != odd y.
proof: Proof. move => cpa eq1. case ox: (odd x); case oy: (odd y) => //. move:(f_equal (fun z => z %% 4) eq1); rewrite -(modnDm) square_odd_mod4 //. rewrite square_odd_mod4 // (@modn_small 1) // (@modn_small 2) //. case oz: (odd z); first by rewrite square_odd_mod4. by rewrite (evenE oz) -mul2n expnMn modnMr. move: cpa; rewrite (evenE ox) (evenE oy) -!muln2 /coprime. by rewrite -muln_gcdl muln_eq1 andbF. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)