proposition: Lemma Qpower_1_lt: forall (q : Q) (n : Z), (1<q)%Q -> (0<n)%Z -> (1 < q ^ n)%Q.
proof: Proof. intros q n Hq Hn. destruct n. - inversion Hn. - apply Qpower_1_lt_pos; assumption. - discriminate (Z.lt_trans _ _ _ Hn (Pos2Z.neg_is_neg p)). Qed.
imports: Zpow_facts Qfield Qreduction