proposition: Lemma less_pres_rht : forall a b :IR, a[<] b -> rht a b [<] b.
proof: Proof. intros. unfold rht in |- *. apply shift_div_less. apply pos_three. rstepr (b[+]Two[*]b). apply plus_resp_less_rht. auto. Qed.
imports: CoRN.reals.CReals1