proposition: Lemma sqrt_cauchy : forall a b c d:R, a * c + b * d <= sqrt (Rsqr a + Rsqr b) * sqrt (Rsqr c + Rsqr d).
proof: Proof. intros a b c d; apply Rsqr_incr_0_var; [ rewrite Rsqr_mult; repeat rewrite Rsqr_sqrt; unfold Rsqr; [ replace ((a * c + b * d) * (a * c + b * d)) with (a * a * c * c + b * b * d * d + 2 * a * b * c * d); [ replace ((a * a + b * b) * (c * c + d * d)) with (a * a * c * c + b * b * d * d + (a * a * d * d + b * b * c * c)); [ apply Rplus_le_compat_l; replace (a * a * d * d + b * b * c * c) with (2 * a * b * c * d + (a * a * d * d + b * b * c * c - 2 * a * b * c * d)); [ pattern (2 * a * b * c * d) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; replace (a * a * d * d + b * b * c * c - 2 * a * b * c * d) with (Rsqr (a * d - b * c)); [ apply Rle_0_sqr | unfold Rsqr; ring ] | ring ] | ring ] | ring ] | apply (Rplus_le_le_0_compat (Rsqr c) (Rsqr d) (Rle_0_sqr c) (Rle_0_sqr d)) | apply (Rplus_le_le_0_compat (Rsqr a) (Rsqr b) (Rle_0_sqr a) (Rle_0_sqr b)) ] | apply Rmult_le_pos; apply sqrt_positivity; apply Rplus_le_le_0_compat; apply Rle_0_sqr ]. Qed.
imports: Rbase Rfunctions Rsqrt_def