proposition: Theorem oppℝ_Eeq_proper_realizer : forall e, oppℝ_Eeq_proper↓e ⊩ ∀x y, (x ≡≡ y → -x ≡≡ -y)%Re.
proof: Proof. unfold Eeq. Ksolve. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions ClassicalRealizability.Real_relations