proposition: Lemma ing_lt : forall x y : F, x [<] y -> inject_Q x [<] inject_Q y.
proof: Proof. intros. simpl in |- *. exists 0. exists ((y[-]x) [/]TwoNZ). apply pos_div_two. apply shift_zero_less_minus. assumption. intros. apply less_leEq; apply pos_div_two'. simpl in |- *. apply shift_zero_less_minus; auto. Qed.
imports: CoRN.algebra.Cauchy_COF CoRN.reals.CReals