proposition: Fact geom x y : 0 < x < y -> x < sqrt (x * y) < (x + y) /2 /\ (x + y) /2 < y.
proof: Proof. intros xPos. assert (Lem := Rmult_le_pos); assert (Ltm := Rmult_lt_0_compat). repeat split; try lra. - assert (x = sqrt (x * x)) by (rewrite sqrt_square; lra). assert (sqrt (x * x) < sqrt (x * y)); try lra. apply sqrt_lt_1; try (apply Lem; lra). apply Rmult_lt_compat_l; lra. - replace ((x + y) / 2) with (sqrt (((x + y) / 2) * ((x + y) / 2))); [idtac | rewrite sqrt_square; lra]. apply sqrt_lt_1; try (apply Lem; lra). replace ((x + y) / 2 * ((x + y) / 2)) with (((y - x) * (y - x)) /4 + x * y); [idtac|field]. assert (0 < (y - x) * (y - x) / 4); repeat apply Ltm; lra. Qed.
imports: Reals Psatz