proposition: Theorem oppℝ_Req_proper_realizer : forall e, oppℝ_Req_proper↓e ⊩ ∀x y, (x ≡ y → -x ≡ -y)%Re.
proof: Proof. unfold oppℝ. Kmove. exists ε₁. find. replace (- q₁ - - q₂) with (-(q₁ - q₂)) by ring. now rewrite Qcabs_opp. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions ClassicalRealizability.Real_relations