proposition: Lemma Qarchimedean_power2_pos : forall q : Q, {p : positive | (q < Z.pos (2^p) # 1)%Q}.
proof: Proof. intros q. destruct (Qarchimedean q) as [pexp Hpexp]. exists (Pos.size pexp). pose proof Pos.size_gt pexp as H1. unfold Qlt in *. cbn in *; Zify.zify. apply (Z.mul_lt_mono_pos_r (QDen q)) in H1; [|assumption]. apply (Z.lt_trans _ _ _ Hpexp H1). Qed.
imports: Zpow_facts Qfield Qreduction