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