proposition: Lemma Qpower_lt_compat_l: forall (q : Q) (n m : Z), (n < m)%Z -> (1<q)%Q -> (q ^ n < q ^ m)%Q.
proof: Proof. intros q n m Hnm Hq. replace m with (n+(m-n))%Z by ring. rewrite Qpower_plus, <- Qmult_1_r, <- Qmult_assoc. 2: { intros Habsurd. rewrite Habsurd in Hq. discriminate Hq. } rewrite Qmult_lt_l, Qmult_1_l. 2: { apply Qpower_0_lt. exact (Qlt_trans 0 1 q ltac:(reflexivity) Hq). } remember (m-n)%Z as k. apply Qpower_1_lt. - exact Hq. - rewrite Heqk; apply Z.lt_0_sub, Hnm. Qed.
imports: Zpow_facts Qfield Qreduction