proposition: Lemma Fermat2_bound a b c: a^2 + b^2 = c^2 -> b <= c ?= iff (a == 0).
proof: Proof. move => h. by rewrite - (mono_leqif leq_sqr) - h - {1} (add0n (b^2)) (mono_leqif (leq_add2r (b^2))) -[0]/(0^2) (mono_leqif leq_sqr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)