proposition: Lemma leif_rootC_AGM (I : finType) (A : {pred I}) (n := #|A|) E : {in A, forall i, 0 <= E i} -> n.-root (\prod_(i in A) E i) <= (\sum_(i in A) E i) / n%:R ?= iff [forall i in A, forall j in A, E i == E j].
proof: Proof. move=> Ege0; have [n0 | n_gt0] := posnP n. rewrite n0 root0C invr0 mulr0; apply/leif_refl/forall_inP=> i. by rewrite (card0_eq n0). rewrite -(mono_in_leif (ler_pXn2r n_gt0)) ?rootCK //=; first 1 last. - by rewrite qualifE /= rootC_ge0 // prodr_ge0. - by rewrite rpred_div ?rpred_nat ?rpred_sum. exact: leif_AGM. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)