proposition: Lemma mean_aux x1 y1 x2 y2 : 0 <= x1 -> 0 <= y1 -> x1 <= x2 -> y1 <= y2 -> sqrt (x1 * y1) = (x2 + y2) / 2 -> x1 = x2 /\ y1 = y2 /\ x1 = y1.
proof: Proof. intros px py lx ly E. assert (sqrt (x1 * y1) <= sqrt (x2 * y2)). { apply sqrt_le_1; try apply Rmult_le_pos; auto. - apply Rle_trans with x1; eauto. - apply Rle_trans with y1; eauto. - apply Rmult_le_compat; eauto. } pose proof mean2 x1 y1 px py. pose proof mean2 x2 y2 ltac:(lra) ltac:(lra). pose proof mean2_ge x1 y1 px py ltac:(lra). pose proof mean2_ge x2 y2 ltac:(lra) ltac:(lra) ltac:(lra). subst y1 y2. change (x1 * x1) with (x1 ²) in E. rewrite sqrt_Rsqr in E; auto. unfold Rdiv in E. rewrite Rmult_plus_distr_r in E. rewrite Rdiv_fold in E. rewrite <-double_var in E. auto. Qed.
imports: Lia Reals Psatz