proposition: Lemma pow_mon3 x y z: T1nf x -> x <= y -> x ^z <= y ^z.
proof: Proof. move => nx xy. have sa: forall n, T1nf (exp_F x n) by move => n;rewrite nf_expF. rewrite /T1exp; apply: T1le_mul => //; last first. elim (T1split z).2; first by rewrite T1lenn. by move => n; rewrite /exp_F -/exp_F => h; apply:T1le_mul. set w := (T1div_by_omega (T1split z).1). rewrite /exp_O. case xz: (x== zero). case wz: (w== zero); first by rewrite (eqP wz) !T1muln0 !if_same T1lenn. by rewrite (eqP xz) T1le0n. case yz: (y== zero); first by move:xy; rewrite (eqP yz) T1len0 xz. case xo: (x== one). rewrite T1ge1; case (y== one) => //; case (T1finite y) => //. case yo: (y== one). by move: xy; rewrite (eqP yo); rewrite T1le_eqVlt xo T1lt1 xz. case fx: (T1finite x). case y => // a n b /=; case a => // a' n' b' /=. by rewrite andbF phi0_le T1le_pmull. case fy: (T1finite y). move: xy fx fy; case x => // a n b; case a => // a' n' b' /=. by case y => // a'' n'' b'' //; case a''. rewrite phi0_le; apply: T1le_mul2r; apply: T1le_mul2r. move: xy; case x => //; first by rewrite !T1le0n. by move => a n b; case y => // a' n' b' /=; exact: T1le_cons_le. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)