proposition: Lemma lft_rht : lft [<] rht.
proof: Proof. 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.CPoly_Contin