proposition: Lemma Req_sym_realizer : forall e, Req_sym↓e ⊩ ∀x y, (x ≡ y → y ≡ x)%Re.
proof: Proof. intro. start. rewrite Qcabs_minus,Qcplus_comm in Hπ. Kmove. exists ε₂, ε₁. Ksolve. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions