proposition: Lemma RL_delta2 : delta2 [/]TwoNZ [<] b[-]a.
proof: Proof. apply shift_div_less'. apply pos_two. apply leEq_less_trans with (b[-]a). unfold delta2 in |- *; clear delta2. apply leEq_transitive with csi2. apply Min_leEq_lft. unfold csi2 in |- *. apply Min_leEq_lft. astepl ([0][+] (b[-]a)); rstepr (b[-]a[+] (b[-]a)). apply plus_resp_less_rht. apply shift_less_minus; astepl a; assumption. Qed.
imports: CoRN.ftc.RefSeparating CoRN.ftc.RefSeparated CoRN.ftc.RefSepRef