proposition: Lemma Qpower_lt_compat_l_inv: forall (q : Q) (n m : Z), (q ^ n < q ^ m)%Q -> (1<q)%Q -> (n < m)%Z.
proof: Proof. intros q n m Hnm Hq. destruct (Z_lt_le_dec n m) as [Hd|Hd]. - assumption. - pose proof Qpower_le_compat_l q m n Hd (Qlt_le_weak _ _ Hq) as Hnm'. pose proof Qlt_le_trans _ _ _ Hnm Hnm' as Habsurd. destruct (Qlt_irrefl _ Habsurd). Qed.
imports: Zpow_facts Qfield Qreduction