proposition: Lemma pow_mon1 x y z: T1nf x -> T1nf y -> T1nf z -> x != zero -> y <= z -> x ^y <= x ^z.
proof: Proof. move => nx ny nz xnz yz. rewrite (sub_pr1 nz yz) exp_sum // ? nf_sub // T1le_pmulr // ? nf_exp //. by rewrite exp_eq0 (negbTE xnz). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)