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