proposition: Lemma G_m_n_upper : forall (x : R1) (m n : nat), m <= n -> G x n[<]sndT (Intrvl x m).
proof: Proof. intros. unfold G in |- *. apply less_leEq_trans with (sndT (Intrvl x n)). apply Average_less_Greatest. apply is_interval. apply Intrvl_inside_r_n. assumption. Qed.
imports: CoRN.reals.Q_in_CReals