proposition: Theorem oppℝ_Cauchy_realizer : forall e, oppℝ_Cauchy↓e ⊩ ∀x, Cauchy x → Cauchy (- x).
proof: Proof. intro e. startn 0. apply oppℝ_Req_proper_realizer. do 2 exists x. Ksolve. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions ClassicalRealizability.Real_relations