proposition: Theorem addℝ_Total_realizer : forall e, addℝ_Total↓e ⊩ ∀x, ∀y, Total x → Total y → Total (x + y).
proof: Proof. unfold Total. intro e. start. apply Qq_realizer. exists (ℚ (ε/2)). find. start. apply ℚdiv_realizer. find. assert (0 < ε / 2) by now apply half_pos. do 3 Ksolve. unfold addℝ. Ksolve. now apply eq_half. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions ClassicalRealizability.Real_relations