proposition: Theorem invℝ_Total_realizer : forall e, invℝ_Total↓e ⊩ ∀x, Total x → Cauchy x → x ≠ (embed_ℚ_ℝ 0) → Total (/ x).
proof: Proof. unfold Total, apartℝ. Ksolve. start. apply (prop_guard Ht4). intros [_ ?]. subst. apply Qq_realizer. find. start. apply ℚdiv_realizer. find. find. pose (q' := 1 / (Qcabs q₁ - ε₁ - ε0 / 2)). pose (bound := Qcmin (ε / (q' * q' + Qcabs q' * ε)) (ε0 / 2)). assert (Hq' : 0 < q'). { unfold q'. replace (q₁ - 0) with q₁ in Hc3 by ring. apply Qclt_shift_div_l. + replace ((|q₁|) - ε₁ - ε0 / 2) with ((|q₁|) + - (ε₁ + ε0 / 2)) by ring. rewrite <- Qclt_minus_iff. apply Qclt_le_trans with (ε₁ + ε0 + ε₂); trivial. rewrite Qclt_minus_iff. replace (ε₁ + ε0 + ε₂ + - (ε₁ + ε0 / 2)) with (ε0 - ε0 / 2 + ε₂) by ring. rewrite <- Qcplus_0_l at 1. apply Qcplus_lt_compat; trivial. unfold Qcminus. rewrite <- Qclt_minus_iff. apply Qclt_shift_div_r. now compute. simpl. replace (ε0 * 2%Z) with (ε0 + ε0). rewrite Qclt_minus_iff. ring_simplify. assumption. rewrite Qcmult_comm. Qcunfold. simpl. ring. + rewrite Qcmult_0_l. now compute. } assert (Hmin : 0 < bound). { apply Qc.min_glb_lt. * apply Qclt_shift_div_l. + replace 0 with (0 * q' + q' * 0) by ring. apply Qcplus_lt_compat. - apply Qcmult_lt_compat_r; assumption. - rewrite Qcabs_pos. apply Qcmult_lt_compat_l; assumption. apply Qclt_le_weak; assumption. + rewrite Qcmult_0_l. assumption. * apply half_pos; ok. } start. apply absℚ_realizer. find. start. apply ℚsub_realizer. find. find. start. apply ℚsub_realizer. find. find. start. apply Qq_realizer. find. start. apply ℚdiv_realizer. find. find. find. start. apply absℚ_realizer. find. start. apply ℚmul_realizer. find. find. start. apply ℚadd_realizer. find. find. start. apply ℚdiv_realizer. find. find. start. apply minℚ_realizer. find. find. change 2%Z with (Z.of_nat 2). fold q'. fold bound. start. apply Ht. find. start. apply Qq_realizer. find. start. apply ℚdiv_realizer. find. find. Ksolve. find. assert (Hq : bound < |q|). { replace (q₁ - 0) with q₁ in Hc3 by ring. eapply (conjecture1 x ε ε₁ ε0 ε₂ q₁ q); eassumption. } unfold invℝ. Ksolve. * unfold Qcdiv. rewrite Qcmult_1_l. rewrite Qcabs_inv. rewrite Qcinv_involutive. ok. * clear_realizers. assert (Hqq' : |1 / q| <= |q'|). { assert (Heq : q₁ - 0 = q₁) by ring. rewrite Heq in *. apply (conjecture2 ε ε₁ ε0 ε₂ q₁ q); assumption. } etransitivity. apply Qc.le_min_l. assert (0 < q' * q' + |q'| * ε). { change 0 with (0 + 0). apply Qcplus_lt_compat. apply Qcsquare_pos. symmetry. apply Qclt_not_eq; ok. replace 0 with (0 * ε) by ring. apply Qcmult_lt_compat_r. ok. rewrite Qcabs_pos. ok. apply Qclt_le_weak; ok. } apply Qcmult_le_compat. + apply Qclt_le_weak; ok. + rewrite Qcinv_nonneg. apply Qclt_le_weak. ok. + reflexivity. + apply Qcinv_pos_le_compat. - assert (0 < |1 / q|). { unfold Qcdiv. rewrite Qcmult_1_l. rewrite Qcabs_inv. rewrite Qcinv_pos. transitivity bound; ok. } change 0 with (0 + 0). apply Qcplus_lt_compat. rewrite <- Qcabs_pos. rewrite Qcabs_mult. apply Qcsquare_pos. symmetry. apply Qclt_not_eq. ok. now apply Qcsquare_nonneg. replace 0 with (0 * ε) by ring. apply Qcmult_lt_compat_r; ok. - apply Qcplus_le_compat. setoid_rewrite <- Qcabs_pos at 1 2; try now apply Qcsquare_nonneg. do 2 rewrite Qcabs_mult. apply Qcmult_le_compat; apply Qcabs_nonneg || ok. apply Qcmult_le_compat_r. ok. apply Qclt_le_weak. ok. * unfold Qcdiv. rewrite Qcmult_1_l. rewrite Qcinv_involutive. ok. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions ClassicalRealizability.Real_relations