proposition: Lemma base' x y : (x * y) <= (x + y) * (x + y) / 4.
proof: Proof. pose proof base x y as L. apply Rmult_le_compat_r with (r := / 4) in L. 2:lra. refine (Rle_trans _ _ _ _ L). apply Req_le. rewrite (Rmult_comm _ (/ 4)), <-Rmult_assoc, (Rmult_comm _ 4). rewrite Rinv_r. ring. lra. Qed.
imports: Lia Reals Psatz