proposition: Lemma Qpower_1_le_pos: forall (q : Q) (n : positive), (1<=q)%Q -> (1 <= q ^ (Z.pos n))%Q.
proof: Proof. intros q n Hq. induction n. - cbn in *. apply Qmult_le_1_compat. 1:assumption. apply Qmult_le_1_compat; assumption. - cbn in *. apply Qmult_le_1_compat; assumption. - cbn; assumption. Qed.
imports: Zpow_facts Qfield Qreduction