proposition: Lemma base x y : 4 * (x * y) <= (x + y) * (x + y).
proof: Proof. apply Rminus_le. apply Rle_trans with (- (x - y) ^ 2). - now ring_simplify; auto with *. - apply Rge_le, Ropp_0_le_ge_contravar, pow2_ge_0. Qed.
imports: Lia Reals Psatz