proposition: Theorem addℚ_resp_pos : forall e p q tp tq, (tp↓e ⊩ 0 << p) -> (tq↓e ⊩ 0 << q) -> (tp @ tq)↓e ⊩ 0 << p + q.
proof: Proof. intros e p q tp tq Htp Htq. start. apply (prop_guard Htp). intro Hp. apply Htq. apply (prop_subst_stack Hπ). intro. rewrite <- Qcplus_0_r at 1. now apply Qcplus_lt_compat. Qed.
imports: QArith ClassicalRealizability.Qcabs ClassicalRealizability.Qcminmax ClassicalRealizability.Kbase