proposition: Lemma Qaverage_less_greatest : forall a b : Q, a < b -> (a + b) * (1#2) < b.
proof: Proof. intros. apply (Qmult_lt_r _ _ (2#1)). reflexivity. rewrite <- Qmult_assoc, (Qmult_comm (1#2)), Qmult_inv_r . apply (Qplus_lt_l _ _ (-b)). ring_simplify. exact H. discriminate. Qed.
imports: Coq.QArith.QArith Coq.ZArith.ZArith Coq.NArith.NArith Coq.QArith.Qpower Coq.QArith.Qround Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.List