proposition: Lemma RL_csi1 : [0] [<] csi1.
proof: Proof. unfold csi1 in |- *; apply less_Min. apply shift_less_minus; astepl a; assumption. apply pos_div_two. apply shift_less_minus. astepl (Mesh P); assumption. Qed.
imports: CoRN.ftc.RefSeparating CoRN.ftc.RefSeparated CoRN.ftc.RefSepRef