proposition: Lemma Fermat2_bound2 a b c: a^2 + b^2 = c^2 -> c <= (a+b) ?= iff (a*b == 0).
proof: Proof. move => h. rewrite - (mono_leqif leq_sqr) sqrnD - h - {1} (addn0 (a^2 + b^2)). by rewrite (mono_leqif (leq_add2l (a^2 + b^2))); split => //; case: (a*b). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)