proposition: Lemma pythagore_aux a b c (d := (c %/ b)) : 0 < b -> a * b^2 = c^2 -> c = d * b /\ a = d ^2.
proof: Proof. move => bp h; move: (esym (@dvdn_pexp2r b c 2 (ltnSn 1))). rewrite -h {2}/dvdn modnMl dvdn_eq eqxx => /eqP h1. by move /eqP: h; rewrite -{1 2} h1 expnMn eqn_pmul2r ? sqrn_gt0 // => /eqP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)