proposition: Lemma Qpower_le_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 m n) as [Hd|Hd]. - pose proof Qpower_lt_compat_l q m n Hd Hq as Hnm'. pose proof Qle_lt_trans _ _ _ Hnm Hnm' as Habsurd. destruct (Qlt_irrefl _ Habsurd). - assumption. Qed.
imports: Zpow_facts Qfield Qreduction