proposition: Lemma ler_wpXz2r n (hn : 0 <= n) : {in >= 0 & , {homo (@exprz R)^~ n : x y / x <= y}}.
proof: Proof. by case: n hn=> // n _; exact: lerXn2r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)