proposition: Theorem addℝ_Req_comm_realizer : forall e, addℝ_Req_comm↓e ⊩ ∀x y, Cauchy x → Cauchy y → (x + y ≡ y + x)%Re.
proof: Proof. intro e. startn 16. apply addℝ_Cauchy_realizer. exists x, y. repeat split; try ok. exists ε₁, ε₂, q₁, q₂. find. startn 1. apply addℝ_switch_realizer. find. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions ClassicalRealizability.Real_relations