proposition: Lemma Qmean_property:forall (x y:Q), x < y -> x < Qmean x y /\ Qmean x y < y.
proof: Proof. intros x y H; split; unfold Qmean. apply Qmult_pos_Qlt_Qdiv; auto; stepl (x+x); auto; ring. apply Qmult_pos_Qdiv_Qlt; auto; stepr (y+y); auto; ring. Qed.