proposition: Lemma Qmean_incr: forall x1 x2 y1 y2, x1< x2 -> y1 < y2 -> Qmean x1 y1 < Qmean x2 y2.
proof: Proof. intros x1 x2 y1 y2 Hx Hy; unfold Qmean; apply Qmult_Qdiv_pos; auto; (stepl (x1 + x1 + y1 + y1) by ring); stepr (x2 + x2 + y2 + y2) ; auto; ring. Qed.