proposition: Lemma Req_trans_realizer : forall e, Req_trans↓e ⊩ ∀x y z, Total y → (x ≡ y → y ≡ z → x ≡ z)%Re.
proof: Proof. Ksolve. apply absℚ_tight_realizer. find. start. assert (0 < ε / 2)%Qc by now apply half_pos. assert (0 <= ε / 2)%Qc by now apply Qclt_le_weak. apply Ht. find. startn 3. eapply prop_guard. start. apply Ht0. exists ε₁. find. intro Habs. Kevals. apply Ht1. exists (ε / 2), ε₂. find. apply (prop_subst_stack Hπ). clear_realizers. intro Ha. replace (q₁ - q₂) with ((q₁ - q) + (q - q₂)) by ring. etransitivity. now apply Qcabs_triangle. replace (ε₁ + ε₂ + ε) with (ε₁ + ε/2 + (ε/2 + ε₂)). now apply Qcplus_le_compat. replace (ε₁ + ε / 2 + (ε / 2 + ε₂)) with (ε₁ + ε₂ + (ε / 2+ ε / 2)) by ring. f_equal. now rewrite eq_half. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions