proposition: Lemma RL_Q_P'_sum : AbsIR (Partition_Sum RL_fP'_in_P' incF[-]Partition_Sum RL_fQ_in_Q incF) [<=] alpha.
proof: Proof. apply leEq_wdl with (AbsIR (Partition_Sum RL_fP'_in_P' incF[-] Partition_Sum (sep__sep_points_lemma _ _ _ F contF Hab' _ _ _ _ RL_P'_sep RL_R'_sep _ RL_alpha _ RL_csi3 _ RL_fP'_in_P') incF)). unfold Q, fQ in |- *; apply sep__sep_Sum. apply AbsIR_wd. unfold Partition_Sum in |- *; apply cg_minus_wd. algebra. apply Sumx_wd; intros. algebra. Qed.
imports: CoRN.ftc.RefSeparating CoRN.ftc.RefSeparated CoRN.ftc.RefSepRef