proposition: Lemma G_m_n_lower : forall (x : R1) (m n : nat), m <= n -> fstT (Intrvl x m)[<]G x n.
proof: Proof. intros. unfold G in |- *. apply leEq_less_trans with (fstT (Intrvl x n)). apply Intrvl_inside_l_n. assumption. apply Smallest_less_Average. apply is_interval. Qed.
imports: CoRN.reals.Q_in_CReals