proposition: Theorem Q_is_archemaedian0 : forall x : Q, {n : positive | x<Qmake n 1%positive}.
proof: Proof. intro x. case x. intros p q. exists (P_of_succ_nat (Z.abs_nat p)). red in |- *. unfold Qnum at 1 in |- *. unfold Qden in |- *. apply toCProp_Zlt. simpl in |- *. rewrite Zmult_1_r. apply Z.lt_le_trans with (P_of_succ_nat (Z.abs_nat p) * 1)%Z. rewrite Zmult_1_r. case p; simpl in |- *. auto with zarith. intros; rewrite P_of_succ_nat_o_nat_of_P_eq_succ; rewrite Pplus_one_succ_r. change (p0 < p0 + 1)%Z in |- *. auto with zarith. intros; unfold Z.lt in |- *; auto. change (P_of_succ_nat (Z.abs_nat p) * 1%positive <= P_of_succ_nat (Z.abs_nat p) * q)%Z in |- *. apply Zmult_le_compat_l. change (Z.succ 0 <= q)%Z in |- *. apply Zgt_le_succ. auto with zarith. auto with zarith. Qed.
imports: CoRN.logic.CLogic Coq.Arith.Arith Coq.Arith.Peano_dec CoRN.model.structures.Zsec Coq.QArith.QArith CoRN.stdlib_omissions.Q