proposition: Theorem addℝ_Eeq_comm_realizer : forall e, addℝ_Eeq_comm↓e ⊩ ∀x y, (x + y ≡≡ y + x)%Re.
proof: Proof. Ksolve; startn 0; apply addℝ_switch_realizer; find. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions ClassicalRealizability.Real_relations