proposition: Lemma less_pres_lft : forall a b :IR, a[<] b -> a [<] lft a b.
proof: Proof. intros. unfold lft in |- *. apply shift_less_div. apply pos_three. rstepl (Two[*]a[+]a). apply plus_resp_less_lft. auto. Qed.
imports: CoRN.reals.CReals1