proposition: Lemma ler_wiXn2l x : 0 <= x -> x <= 1 -> {homo GRing.exp x : m n / (n <= m)%N >-> m <= n}.
proof: Proof. move=> xge0 xle1 m n /= hmn. by rewrite -(subnK hmn) exprD ler_piMl ?(exprn_ge0, exprn_ile1). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)