proposition: Lemma mean2_strict x y : 0 <= x -> 0 <= y -> x <> y -> sqrt (x * y) < (x + y) / 2.
proof: Proof. assert (MP : forall x y, 0 <= x -> 0 <= y -> 0 <= x * y). { intros. replace 0 with (0 * 0) by ring. apply Rmult_le_compat; auto with *. } assert (AP : forall x y, 0 <= x -> 0 <= y -> 0 <= x + y) by (intros; lra). assert (0 <= 4) by lra. intros px py n. pose proof base_strict x y n as L. apply sqrt_lt_1 in L. replace 4 with (2 * 2) in L by ring. rewrite sqrt_mult in L. do 2 rewrite sqrt_square in L. apply Rmult_lt_compat_r with (r := / 2) in L. refine (Rle_lt_trans _ _ _ _ L); clear L; apply Req_le. replace (2 * sqrt (x * y) * / 2) with ((2 * / 2) * sqrt (x * y)) by ring. rewrite Rinv_r. ring. all: auto with *; lra. Qed.
imports: Lia Reals Psatz