proposition: Theorem Rlt_proper_realizer : forall e, Rlt_proper↓e ⊩ ∀x₁ x₂ y₁ y₂, Total x₂ → Total y₂ → (x₁ ≡ x₂ → y₁ ≡ y₂ → x₁ << y₁ → x₂ << y₂)%Re.
proof: Proof. intro e. Kmove. eexists; split; [| try eok]. Kmove. apply Qq_realizer. exists (ℚ (ε/5)). find. start. apply ℚdiv_realizer. find. assert (0 < ε / 5) by now apply fifth_pos. assert (0 <= ε / 5)%Qc by now apply Qclt_le_weak. do 2 Ksolve. startn 11. eapply prop_guard. Kmove. exists ε₁. find. now apply Qclt_le_weak. intro Hle₁. eapply prop_guard. Kmove. exists ε₂. find. now apply Qclt_le_weak. intro Hle₂. Ksolve. clear_realizers. apply Qcabs_diff_le_condition in Hle₁. destruct Hle₁ as [_ Hle₁]. apply Qcabs_diff_le_condition in Hle₂. destruct Hle₂ as [Hle₂ _]. transitivity (q₁ + ε₁ + ε / 5 + ε / 5 + ε / 5 + ε / 5). repeat (apply Qcplus_le_compat; [| reflexivity]). now rewrite <- Qcplus_assoc. transitivity (q₂ - (ε₂ + ε / 5)); [| assumption]. apply Qcle_shift_minus_l. replace (q₁ + ε₁ + ε / 5 + ε / 5 + ε / 5 + ε / 5 + (ε₂ + ε / 5)) with (q₁ + ε₁ + (ε / 5 + ε / 5 + ε / 5 + ε / 5 + ε / 5) + ε₂) by ring. replace (ε / 5 + ε / 5 + ε / 5 + ε / 5 + ε / 5) with ε. assumption. Qcunfold. simpl. field. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions