proposition: Lemma U_m_n_V : forall m n : nat, m <= n -> V m[<]U n.
proof: Proof. intros. unfold U in |- *. apply leEq_less_trans with (y := V n). apply V_increase. assumption. unfold V in |- *. apply Smallest_less_Average. apply is_interval. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon