proposition: Lemma RL_P'_Mesh : Mesh P' [<] d.
proof: Proof. unfold P' in |- *. eapply leEq_less_trans. apply sep__part_mon_Mesh. unfold csi1 in |- *. apply shift_plus_less'; eapply leEq_less_trans. apply Min_leEq_rht. apply pos_div_two'. apply shift_less_minus. astepl (Mesh P); assumption. Qed.
imports: CoRN.ftc.RefSeparating CoRN.ftc.RefSeparated CoRN.ftc.RefSepRef