proposition: Lemma pow_mon2 x y z: T1nf x -> T1nf y -> T1nf z -> x != zero -> x != one -> y < z -> x ^y < x ^z.
proof: Proof. move => nx ny nz xnz xn1 yz. have na := (nf_exp nx (nf_sub nz ny)). have nb: x ^ y != zero by rewrite exp_eq0 (negbTE xnz). have nc: x ^ (z - y) != zero by rewrite exp_eq0 (negbTE xnz). rewrite (sub_pr1 nz (T1ltW yz)) exp_sum // ? nf_sub //. rewrite - {1}(T1muln1 (nf_exp nx ny)) T1lt_mul2l// T1lt_neAle eq_sym. by rewrite exp_eq1 ? nf_sub // (negbTE xn1) (sub_nz nz yz) T1ge1 nc. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)