proposition: Lemma U_m_n_W : forall m n : nat, m <= n -> U n[<]W m.
proof: Proof. intros. unfold U in |- *. apply less_leEq_trans with (y := W n). unfold W in |- *. apply Average_less_Greatest. apply is_interval. apply W_decrease. assumption. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon