proposition: Lemma base_strict x y : x <> y -> 4 * (x * y) < (x + y) * (x + y).
proof: Proof. intros ne. apply Rminus_lt. apply Rle_lt_trans with (- (x - y) ^ 2). - now ring_simplify; auto with *. - apply Rgt_lt, Ropp_0_lt_gt_contravar. assert (H : 0 <> x - y) by lra; revert H. generalize (x - y); clear. intros r n. destruct (Rdichotomy _ _ n) as [p|p]. + replace (r ^ 2) with (r * r) by ring. apply Rmult_lt_0_compat; auto. + replace (r ^ 2) with (- r * - r) by ring. apply Rmult_lt_0_compat; auto with *. Qed.
imports: Lia Reals Psatz