proposition: Theorem oppℝ_Total_realizer : forall e, oppℝ_Total↓e ⊩ ∀x, Total x → Total (- x).
proof: Proof. unfold Total,oppℝ. Kmove. findn 3. eexists (_ → Z). find. Ksolve. now rewrite Qcopp_involutive. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions ClassicalRealizability.Real_relations