proposition: Lemma RL_P'_P_sum : AbsIR (Partition_Sum HfP incF[-]Partition_Sum RL_fP'_in_P' incF) [<=] alpha.
proof: Proof. apply leEq_wdl with (AbsIR (Partition_Sum HfP incF[-] Partition_Sum (sep__part_pts_in_Partition _ _ _ F contF Hab' _ P _ RL_alpha _ RL_csi1 RL_delta1 _ HfP) incF)). apply sep__part_Sum. assumption. apply AbsIR_wd; apply cg_minus_wd. algebra. unfold Partition_Sum in |- *; apply Sumx_wd; intros. algebra. Qed.
imports: CoRN.ftc.RefSeparating CoRN.ftc.RefSeparated CoRN.ftc.RefSepRef