proposition: Lemma Rle_trans_realizer : forall e, Rle_trans↓e ⊩ ∀x y z, Total y → (x <= y → y <= z → x <= z)%Re.
proof: Proof. Ksolve. apply leℚ_tight_realizer. find. find. start. apply Qq_realizer. find. start. apply ℚdiv_realizer. find. find. start. apply Ht. exists (ε/2). Kmove. now apply half_pos. find. find. startn 3. eapply prop_guard. Kmove. apply Qq_realizer. find. start. apply ℚdiv_realizer. find. find. Kmove. exists ε₁, (ε / 2). find. now apply Qclt_le_weak, half_pos. find. intro Habs. Kmove. apply Qq_realizer. find. start. apply ℚdiv_realizer. find. find. Kmove. exists (ε / 2). find. now apply Qclt_le_weak, half_pos. Ksolve. apply (prop_subst_stack Hπ). clear_realizers. intro Ha. etransitivity. apply Habs. etransitivity. apply Qcplus_le_compat. apply Qcplus_le_compat. apply Ha. reflexivity. reflexivity. setoid_replace ε with (ε / 2 + ε / 2) at 3 by (Qcunfold; destruct ε; simpl; field). replace (q₂ + ε / 2 + ε₂ + ε₁ + ε / 2) with (q₂ + ε₁ + ε₂ + (ε / 2 + ε / 2)) by ring. reflexivity. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions