proposition: Lemma nat_AGM2 m n : 4 * (m * n) <= (m + n) ^ 2 ?= iff (m == n).
proof: Proof. rewrite -[4]/(2 * 2) -mulnA mul2n -addnn sqrnD; apply/leqifP. by rewrite ltn_add2r eqn_add2r ltn_neqAle !nat_Cauchy; case: eqVneq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring