proposition: Lemma addℝ_switch_realizer : forall e, addℝ_switch↓e ⊩ ∀x y ε q, (x + y)%Re ε q → (y + x)%Re ε q.
proof: Proof. unfold addℝ at 1. Ksolve. unfold addℝ. Kmove. exists ε₂, ε₁. find; now rewrite Qcplus_comm. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions ClassicalRealizability.Real_relations