diff options
Diffstat (limited to 'theories/Reals/R_sqr.v')
| -rw-r--r-- | theories/Reals/R_sqr.v | 460 |
1 files changed, 247 insertions, 213 deletions
diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v index d87adc24..270ea6da 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -6,325 +6,359 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: R_sqr.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: R_sqr.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import Rbase. Require Import Rbasic_fun. Open Local Scope R_scope. (****************************************************) -(* Rsqr : some results *) +(** Rsqr : some results *) (****************************************************) Ltac ring_Rsqr := unfold Rsqr in |- *; ring. Lemma Rsqr_neg : forall x:R, Rsqr x = Rsqr (- x). -intros; ring_Rsqr. +Proof. + intros; ring_Rsqr. Qed. Lemma Rsqr_mult : forall x y:R, Rsqr (x * y) = Rsqr x * Rsqr y. -intros; ring_Rsqr. +Proof. + intros; ring_Rsqr. Qed. Lemma Rsqr_plus : forall x y:R, Rsqr (x + y) = Rsqr x + Rsqr y + 2 * x * y. -intros; ring_Rsqr. +Proof. + intros; ring_Rsqr. Qed. Lemma Rsqr_minus : forall x y:R, Rsqr (x - y) = Rsqr x + Rsqr y - 2 * x * y. -intros; ring_Rsqr. +Proof. + intros; ring_Rsqr. Qed. Lemma Rsqr_neg_minus : forall x y:R, Rsqr (x - y) = Rsqr (y - x). -intros; ring_Rsqr. +Proof. + intros; ring_Rsqr. Qed. Lemma Rsqr_1 : Rsqr 1 = 1. -ring_Rsqr. +Proof. + ring_Rsqr. Qed. Lemma Rsqr_gt_0_0 : forall x:R, 0 < Rsqr x -> x <> 0. -intros; red in |- *; intro; rewrite H0 in H; rewrite Rsqr_0 in H; - elim (Rlt_irrefl 0 H). +Proof. + intros; red in |- *; intro; rewrite H0 in H; rewrite Rsqr_0 in H; + elim (Rlt_irrefl 0 H). Qed. Lemma Rsqr_pos_lt : forall x:R, x <> 0 -> 0 < Rsqr x. -intros; case (Rtotal_order 0 x); intro; - [ unfold Rsqr in |- *; apply Rmult_lt_0_compat; assumption - | elim H0; intro; - [ elim H; symmetry in |- *; exact H1 - | rewrite Rsqr_neg; generalize (Ropp_lt_gt_contravar x 0 H1); - rewrite Ropp_0; intro; unfold Rsqr in |- *; - apply Rmult_lt_0_compat; assumption ] ]. +Proof. + intros; case (Rtotal_order 0 x); intro; + [ unfold Rsqr in |- *; apply Rmult_lt_0_compat; assumption + | elim H0; intro; + [ elim H; symmetry in |- *; exact H1 + | rewrite Rsqr_neg; generalize (Ropp_lt_gt_contravar x 0 H1); + rewrite Ropp_0; intro; unfold Rsqr in |- *; + apply Rmult_lt_0_compat; assumption ] ]. Qed. Lemma Rsqr_div : forall x y:R, y <> 0 -> Rsqr (x / y) = Rsqr x / Rsqr y. -intros; unfold Rsqr in |- *. -unfold Rdiv in |- *. -rewrite Rinv_mult_distr. -repeat rewrite Rmult_assoc. -apply Rmult_eq_compat_l. -pattern x at 2 in |- *; rewrite Rmult_comm. -repeat rewrite Rmult_assoc. -apply Rmult_eq_compat_l. -reflexivity. -assumption. -assumption. +Proof. + intros; unfold Rsqr in |- *. + unfold Rdiv in |- *. + rewrite Rinv_mult_distr. + repeat rewrite Rmult_assoc. + apply Rmult_eq_compat_l. + pattern x at 2 in |- *; rewrite Rmult_comm. + repeat rewrite Rmult_assoc. + apply Rmult_eq_compat_l. + reflexivity. + assumption. + assumption. Qed. Lemma Rsqr_eq_0 : forall x:R, Rsqr x = 0 -> x = 0. -unfold Rsqr in |- *; intros; generalize (Rmult_integral x x H); intro; - elim H0; intro; assumption. +Proof. + unfold Rsqr in |- *; intros; generalize (Rmult_integral x x H); intro; + elim H0; intro; assumption. Qed. Lemma Rsqr_minus_plus : forall a b:R, (a - b) * (a + b) = Rsqr a - Rsqr b. -intros; ring_Rsqr. +Proof. + intros; ring_Rsqr. Qed. Lemma Rsqr_plus_minus : forall a b:R, (a + b) * (a - b) = Rsqr a - Rsqr b. -intros; ring_Rsqr. +Proof. + intros; ring_Rsqr. Qed. Lemma Rsqr_incr_0 : - forall x y:R, Rsqr x <= Rsqr y -> 0 <= x -> 0 <= y -> x <= y. -intros; case (Rle_dec x y); intro; - [ assumption - | cut (y < x); - [ intro; unfold Rsqr in H; - generalize (Rmult_le_0_lt_compat y x y x H1 H1 H2 H2); - intro; generalize (Rle_lt_trans (x * x) (y * y) (x * x) H H3); - intro; elim (Rlt_irrefl (x * x) H4) - | auto with real ] ]. + forall x y:R, Rsqr x <= Rsqr y -> 0 <= x -> 0 <= y -> x <= y. +Proof. + intros; case (Rle_dec x y); intro; + [ assumption + | cut (y < x); + [ intro; unfold Rsqr in H; + generalize (Rmult_le_0_lt_compat y x y x H1 H1 H2 H2); + intro; generalize (Rle_lt_trans (x * x) (y * y) (x * x) H H3); + intro; elim (Rlt_irrefl (x * x) H4) + | auto with real ] ]. Qed. Lemma Rsqr_incr_0_var : forall x y:R, Rsqr x <= Rsqr y -> 0 <= y -> x <= y. -intros; case (Rle_dec x y); intro; - [ assumption - | cut (y < x); - [ intro; unfold Rsqr in H; - generalize (Rmult_le_0_lt_compat y x y x H0 H0 H1 H1); - intro; generalize (Rle_lt_trans (x * x) (y * y) (x * x) H H2); - intro; elim (Rlt_irrefl (x * x) H3) - | auto with real ] ]. +Proof. + intros; case (Rle_dec x y); intro; + [ assumption + | cut (y < x); + [ intro; unfold Rsqr in H; + generalize (Rmult_le_0_lt_compat y x y x H0 H0 H1 H1); + intro; generalize (Rle_lt_trans (x * x) (y * y) (x * x) H H2); + intro; elim (Rlt_irrefl (x * x) H3) + | auto with real ] ]. Qed. Lemma Rsqr_incr_1 : - forall x y:R, x <= y -> 0 <= x -> 0 <= y -> Rsqr x <= Rsqr y. -intros; unfold Rsqr in |- *; apply Rmult_le_compat; assumption. + forall x y:R, x <= y -> 0 <= x -> 0 <= y -> Rsqr x <= Rsqr y. +Proof. + intros; unfold Rsqr in |- *; apply Rmult_le_compat; assumption. Qed. Lemma Rsqr_incrst_0 : - forall x y:R, Rsqr x < Rsqr y -> 0 <= x -> 0 <= y -> x < y. -intros; case (Rtotal_order x y); intro; - [ assumption - | elim H2; intro; - [ rewrite H3 in H; elim (Rlt_irrefl (Rsqr y) H) - | generalize (Rmult_le_0_lt_compat y x y x H1 H1 H3 H3); intro; - unfold Rsqr in H; generalize (Rlt_trans (x * x) (y * y) (x * x) H H4); - intro; elim (Rlt_irrefl (x * x) H5) ] ]. + forall x y:R, Rsqr x < Rsqr y -> 0 <= x -> 0 <= y -> x < y. +Proof. + intros; case (Rtotal_order x y); intro; + [ assumption + | elim H2; intro; + [ rewrite H3 in H; elim (Rlt_irrefl (Rsqr y) H) + | generalize (Rmult_le_0_lt_compat y x y x H1 H1 H3 H3); intro; + unfold Rsqr in H; generalize (Rlt_trans (x * x) (y * y) (x * x) H H4); + intro; elim (Rlt_irrefl (x * x) H5) ] ]. Qed. Lemma Rsqr_incrst_1 : - forall x y:R, x < y -> 0 <= x -> 0 <= y -> Rsqr x < Rsqr y. -intros; unfold Rsqr in |- *; apply Rmult_le_0_lt_compat; assumption. + forall x y:R, x < y -> 0 <= x -> 0 <= y -> Rsqr x < Rsqr y. +Proof. + intros; unfold Rsqr in |- *; apply Rmult_le_0_lt_compat; assumption. Qed. Lemma Rsqr_neg_pos_le_0 : - forall x y:R, Rsqr x <= Rsqr y -> 0 <= y -> - y <= x. -intros; case (Rcase_abs x); intro. -generalize (Ropp_lt_gt_contravar x 0 r); rewrite Ropp_0; intro; - generalize (Rlt_le 0 (- x) H1); intro; rewrite (Rsqr_neg x) in H; - generalize (Rsqr_incr_0 (- x) y H H2 H0); intro; - rewrite <- (Ropp_involutive x); apply Ropp_ge_le_contravar; - apply Rle_ge; assumption. -apply Rle_trans with 0; - [ rewrite <- Ropp_0; apply Ropp_ge_le_contravar; apply Rle_ge; assumption - | apply Rge_le; assumption ]. + forall x y:R, Rsqr x <= Rsqr y -> 0 <= y -> - y <= x. +Proof. + intros; case (Rcase_abs x); intro. + generalize (Ropp_lt_gt_contravar x 0 r); rewrite Ropp_0; intro; + generalize (Rlt_le 0 (- x) H1); intro; rewrite (Rsqr_neg x) in H; + generalize (Rsqr_incr_0 (- x) y H H2 H0); intro; + rewrite <- (Ropp_involutive x); apply Ropp_ge_le_contravar; + apply Rle_ge; assumption. + apply Rle_trans with 0; + [ rewrite <- Ropp_0; apply Ropp_ge_le_contravar; apply Rle_ge; assumption + | apply Rge_le; assumption ]. Qed. Lemma Rsqr_neg_pos_le_1 : - forall x y:R, - y <= x -> x <= y -> 0 <= y -> Rsqr x <= Rsqr y. -intros; case (Rcase_abs x); intro. -generalize (Ropp_lt_gt_contravar x 0 r); rewrite Ropp_0; intro; - generalize (Rlt_le 0 (- x) H2); intro; - generalize (Ropp_le_ge_contravar (- y) x H); rewrite Ropp_involutive; - intro; generalize (Rge_le y (- x) H4); intro; rewrite (Rsqr_neg x); - apply Rsqr_incr_1; assumption. -generalize (Rge_le x 0 r); intro; apply Rsqr_incr_1; assumption. + forall x y:R, - y <= x -> x <= y -> 0 <= y -> Rsqr x <= Rsqr y. +Proof. + intros; case (Rcase_abs x); intro. + generalize (Ropp_lt_gt_contravar x 0 r); rewrite Ropp_0; intro; + generalize (Rlt_le 0 (- x) H2); intro; + generalize (Ropp_le_ge_contravar (- y) x H); rewrite Ropp_involutive; + intro; generalize (Rge_le y (- x) H4); intro; rewrite (Rsqr_neg x); + apply Rsqr_incr_1; assumption. + generalize (Rge_le x 0 r); intro; apply Rsqr_incr_1; assumption. Qed. Lemma neg_pos_Rsqr_le : forall x y:R, - y <= x -> x <= y -> Rsqr x <= Rsqr y. -intros; case (Rcase_abs x); intro. -generalize (Ropp_lt_gt_contravar x 0 r); rewrite Ropp_0; intro; - generalize (Ropp_le_ge_contravar (- y) x H); rewrite Ropp_involutive; - intro; generalize (Rge_le y (- x) H2); intro; generalize (Rlt_le 0 (- x) H1); - intro; generalize (Rle_trans 0 (- x) y H4 H3); intro; - rewrite (Rsqr_neg x); apply Rsqr_incr_1; assumption. -generalize (Rge_le x 0 r); intro; generalize (Rle_trans 0 x y H1 H0); intro; - apply Rsqr_incr_1; assumption. +Proof. + intros; case (Rcase_abs x); intro. + generalize (Ropp_lt_gt_contravar x 0 r); rewrite Ropp_0; intro; + generalize (Ropp_le_ge_contravar (- y) x H); rewrite Ropp_involutive; + intro; generalize (Rge_le y (- x) H2); intro; generalize (Rlt_le 0 (- x) H1); + intro; generalize (Rle_trans 0 (- x) y H4 H3); intro; + rewrite (Rsqr_neg x); apply Rsqr_incr_1; assumption. + generalize (Rge_le x 0 r); intro; generalize (Rle_trans 0 x y H1 H0); intro; + apply Rsqr_incr_1; assumption. Qed. Lemma Rsqr_abs : forall x:R, Rsqr x = Rsqr (Rabs x). -intro; unfold Rabs in |- *; case (Rcase_abs x); intro; - [ apply Rsqr_neg | reflexivity ]. +Proof. + intro; unfold Rabs in |- *; case (Rcase_abs x); intro; + [ apply Rsqr_neg | reflexivity ]. Qed. Lemma Rsqr_le_abs_0 : forall x y:R, Rsqr x <= Rsqr y -> Rabs x <= Rabs y. -intros; apply Rsqr_incr_0; repeat rewrite <- Rsqr_abs; - [ assumption | apply Rabs_pos | apply Rabs_pos ]. +Proof. + intros; apply Rsqr_incr_0; repeat rewrite <- Rsqr_abs; + [ assumption | apply Rabs_pos | apply Rabs_pos ]. Qed. Lemma Rsqr_le_abs_1 : forall x y:R, Rabs x <= Rabs y -> Rsqr x <= Rsqr y. -intros; rewrite (Rsqr_abs x); rewrite (Rsqr_abs y); - apply (Rsqr_incr_1 (Rabs x) (Rabs y) H (Rabs_pos x) (Rabs_pos y)). +Proof. + intros; rewrite (Rsqr_abs x); rewrite (Rsqr_abs y); + apply (Rsqr_incr_1 (Rabs x) (Rabs y) H (Rabs_pos x) (Rabs_pos y)). Qed. Lemma Rsqr_lt_abs_0 : forall x y:R, Rsqr x < Rsqr y -> Rabs x < Rabs y. -intros; apply Rsqr_incrst_0; repeat rewrite <- Rsqr_abs; - [ assumption | apply Rabs_pos | apply Rabs_pos ]. +Proof. + intros; apply Rsqr_incrst_0; repeat rewrite <- Rsqr_abs; + [ assumption | apply Rabs_pos | apply Rabs_pos ]. Qed. Lemma Rsqr_lt_abs_1 : forall x y:R, Rabs x < Rabs y -> Rsqr x < Rsqr y. -intros; rewrite (Rsqr_abs x); rewrite (Rsqr_abs y); - apply (Rsqr_incrst_1 (Rabs x) (Rabs y) H (Rabs_pos x) (Rabs_pos y)). +Proof. + intros; rewrite (Rsqr_abs x); rewrite (Rsqr_abs y); + apply (Rsqr_incrst_1 (Rabs x) (Rabs y) H (Rabs_pos x) (Rabs_pos y)). Qed. Lemma Rsqr_inj : forall x y:R, 0 <= x -> 0 <= y -> Rsqr x = Rsqr y -> x = y. -intros; generalize (Rle_le_eq (Rsqr x) (Rsqr y)); intro; elim H2; intros _ H3; - generalize (H3 H1); intro; elim H4; intros; apply Rle_antisym; - apply Rsqr_incr_0; assumption. +Proof. + intros; generalize (Rle_le_eq (Rsqr x) (Rsqr y)); intro; elim H2; intros _ H3; + generalize (H3 H1); intro; elim H4; intros; apply Rle_antisym; + apply Rsqr_incr_0; assumption. Qed. Lemma Rsqr_eq_abs_0 : forall x y:R, Rsqr x = Rsqr y -> Rabs x = Rabs y. -intros; unfold Rabs in |- *; case (Rcase_abs x); case (Rcase_abs y); intros. -rewrite (Rsqr_neg x) in H; rewrite (Rsqr_neg y) in H; - generalize (Ropp_lt_gt_contravar y 0 r); - generalize (Ropp_lt_gt_contravar x 0 r0); rewrite Ropp_0; - intros; generalize (Rlt_le 0 (- x) H0); generalize (Rlt_le 0 (- y) H1); - intros; apply Rsqr_inj; assumption. -rewrite (Rsqr_neg x) in H; generalize (Rge_le y 0 r); intro; - generalize (Ropp_lt_gt_contravar x 0 r0); rewrite Ropp_0; - intro; generalize (Rlt_le 0 (- x) H1); intro; apply Rsqr_inj; - assumption. -rewrite (Rsqr_neg y) in H; generalize (Rge_le x 0 r0); intro; - generalize (Ropp_lt_gt_contravar y 0 r); rewrite Ropp_0; - intro; generalize (Rlt_le 0 (- y) H1); intro; apply Rsqr_inj; - assumption. -generalize (Rge_le x 0 r0); generalize (Rge_le y 0 r); intros; apply Rsqr_inj; - assumption. +Proof. + intros; unfold Rabs in |- *; case (Rcase_abs x); case (Rcase_abs y); intros. + rewrite (Rsqr_neg x) in H; rewrite (Rsqr_neg y) in H; + generalize (Ropp_lt_gt_contravar y 0 r); + generalize (Ropp_lt_gt_contravar x 0 r0); rewrite Ropp_0; + intros; generalize (Rlt_le 0 (- x) H0); generalize (Rlt_le 0 (- y) H1); + intros; apply Rsqr_inj; assumption. + rewrite (Rsqr_neg x) in H; generalize (Rge_le y 0 r); intro; + generalize (Ropp_lt_gt_contravar x 0 r0); rewrite Ropp_0; + intro; generalize (Rlt_le 0 (- x) H1); intro; apply Rsqr_inj; + assumption. + rewrite (Rsqr_neg y) in H; generalize (Rge_le x 0 r0); intro; + generalize (Ropp_lt_gt_contravar y 0 r); rewrite Ropp_0; + intro; generalize (Rlt_le 0 (- y) H1); intro; apply Rsqr_inj; + assumption. + generalize (Rge_le x 0 r0); generalize (Rge_le y 0 r); intros; apply Rsqr_inj; + assumption. Qed. Lemma Rsqr_eq_asb_1 : forall x y:R, Rabs x = Rabs y -> Rsqr x = Rsqr y. -intros; cut (Rsqr (Rabs x) = Rsqr (Rabs y)). -intro; repeat rewrite <- Rsqr_abs in H0; assumption. -rewrite H; reflexivity. +Proof. + intros; cut (Rsqr (Rabs x) = Rsqr (Rabs y)). + intro; repeat rewrite <- Rsqr_abs in H0; assumption. + rewrite H; reflexivity. Qed. Lemma triangle_rectangle : - forall x y z:R, - 0 <= z -> Rsqr x + Rsqr y <= Rsqr z -> - z <= x <= z /\ - z <= y <= z. -intros; - generalize (plus_le_is_le (Rsqr x) (Rsqr y) (Rsqr z) (Rle_0_sqr y) H0); - rewrite Rplus_comm in H0; - generalize (plus_le_is_le (Rsqr y) (Rsqr x) (Rsqr z) (Rle_0_sqr x) H0); - intros; split; - [ split; - [ apply Rsqr_neg_pos_le_0; assumption - | apply Rsqr_incr_0_var; assumption ] - | split; - [ apply Rsqr_neg_pos_le_0; assumption - | apply Rsqr_incr_0_var; assumption ] ]. + forall x y z:R, + 0 <= z -> Rsqr x + Rsqr y <= Rsqr z -> - z <= x <= z /\ - z <= y <= z. +Proof. + intros; + generalize (plus_le_is_le (Rsqr x) (Rsqr y) (Rsqr z) (Rle_0_sqr y) H0); + rewrite Rplus_comm in H0; + generalize (plus_le_is_le (Rsqr y) (Rsqr x) (Rsqr z) (Rle_0_sqr x) H0); + intros; split; + [ split; + [ apply Rsqr_neg_pos_le_0; assumption + | apply Rsqr_incr_0_var; assumption ] + | split; + [ apply Rsqr_neg_pos_le_0; assumption + | apply Rsqr_incr_0_var; assumption ] ]. Qed. Lemma triangle_rectangle_lt : - forall x y z:R, - Rsqr x + Rsqr y < Rsqr z -> Rabs x < Rabs z /\ Rabs y < Rabs z. -intros; split; - [ generalize (plus_lt_is_lt (Rsqr x) (Rsqr y) (Rsqr z) (Rle_0_sqr y) H); - intro; apply Rsqr_lt_abs_0; assumption - | rewrite Rplus_comm in H; - generalize (plus_lt_is_lt (Rsqr y) (Rsqr x) (Rsqr z) (Rle_0_sqr x) H); - intro; apply Rsqr_lt_abs_0; assumption ]. + forall x y z:R, + Rsqr x + Rsqr y < Rsqr z -> Rabs x < Rabs z /\ Rabs y < Rabs z. +Proof. + intros; split; + [ generalize (plus_lt_is_lt (Rsqr x) (Rsqr y) (Rsqr z) (Rle_0_sqr y) H); + intro; apply Rsqr_lt_abs_0; assumption + | rewrite Rplus_comm in H; + generalize (plus_lt_is_lt (Rsqr y) (Rsqr x) (Rsqr z) (Rle_0_sqr x) H); + intro; apply Rsqr_lt_abs_0; assumption ]. Qed. Lemma triangle_rectangle_le : - forall x y z:R, - Rsqr x + Rsqr y <= Rsqr z -> Rabs x <= Rabs z /\ Rabs y <= Rabs z. -intros; split; - [ generalize (plus_le_is_le (Rsqr x) (Rsqr y) (Rsqr z) (Rle_0_sqr y) H); - intro; apply Rsqr_le_abs_0; assumption - | rewrite Rplus_comm in H; - generalize (plus_le_is_le (Rsqr y) (Rsqr x) (Rsqr z) (Rle_0_sqr x) H); - intro; apply Rsqr_le_abs_0; assumption ]. + forall x y z:R, + Rsqr x + Rsqr y <= Rsqr z -> Rabs x <= Rabs z /\ Rabs y <= Rabs z. +Proof. + intros; split; + [ generalize (plus_le_is_le (Rsqr x) (Rsqr y) (Rsqr z) (Rle_0_sqr y) H); + intro; apply Rsqr_le_abs_0; assumption + | rewrite Rplus_comm in H; + generalize (plus_le_is_le (Rsqr y) (Rsqr x) (Rsqr z) (Rle_0_sqr x) H); + intro; apply Rsqr_le_abs_0; assumption ]. Qed. Lemma Rsqr_inv : forall x:R, x <> 0 -> Rsqr (/ x) = / Rsqr x. -intros; unfold Rsqr in |- *. -rewrite Rinv_mult_distr; try reflexivity || assumption. +Proof. + intros; unfold Rsqr in |- *. + rewrite Rinv_mult_distr; try reflexivity || assumption. Qed. Lemma canonical_Rsqr : - forall (a:nonzeroreal) (b c x:R), - a * Rsqr x + b * x + c = - a * Rsqr (x + b / (2 * a)) + (4 * a * c - Rsqr b) / (4 * a). -intros. -rewrite Rsqr_plus. -repeat rewrite Rmult_plus_distr_l. -repeat rewrite Rplus_assoc. -apply Rplus_eq_compat_l. -unfold Rdiv, Rminus in |- *. -replace (2 * 1 + 2 * 1) with 4; [ idtac | ring ]. -rewrite (Rmult_plus_distr_r (4 * a * c) (- Rsqr b) (/ (4 * a))). -rewrite Rsqr_mult. -repeat rewrite Rinv_mult_distr. -repeat rewrite (Rmult_comm a). -repeat rewrite Rmult_assoc. -rewrite <- Rinv_l_sym. -rewrite Rmult_1_r. -rewrite (Rmult_comm 2). -repeat rewrite Rmult_assoc. -rewrite <- Rinv_l_sym. -rewrite Rmult_1_r. -rewrite (Rmult_comm (/ 2)). -rewrite (Rmult_comm 2). -repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym. -rewrite Rmult_1_r. -rewrite (Rmult_comm a). -repeat rewrite Rmult_assoc. -rewrite <- Rinv_l_sym. -rewrite Rmult_1_r. -rewrite (Rmult_comm 2). -repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym. -rewrite Rmult_1_r. -repeat rewrite Rplus_assoc. -rewrite (Rplus_comm (Rsqr b * (Rsqr (/ a * / 2) * a))). -repeat rewrite Rplus_assoc. -rewrite (Rmult_comm x). -apply Rplus_eq_compat_l. -rewrite (Rmult_comm (/ a)). -unfold Rsqr in |- *; repeat rewrite Rmult_assoc. -rewrite <- Rinv_l_sym. -rewrite Rmult_1_r. -ring. -apply (cond_nonzero a). -discrR. -apply (cond_nonzero a). -discrR. -discrR. -apply (cond_nonzero a). -discrR. -discrR. -discrR. -apply (cond_nonzero a). -discrR. -apply (cond_nonzero a). + forall (a:nonzeroreal) (b c x:R), + a * Rsqr x + b * x + c = + a * Rsqr (x + b / (2 * a)) + (4 * a * c - Rsqr b) / (4 * a). +Proof. + intros. + rewrite Rsqr_plus. + repeat rewrite Rmult_plus_distr_l. + repeat rewrite Rplus_assoc. + apply Rplus_eq_compat_l. + unfold Rdiv, Rminus in |- *. + replace (2 * 1 + 2 * 1) with 4; [ idtac | ring ]. + rewrite (Rmult_plus_distr_r (4 * a * c) (- Rsqr b) (/ (4 * a))). + rewrite Rsqr_mult. + repeat rewrite Rinv_mult_distr. + repeat rewrite (Rmult_comm a). + repeat rewrite Rmult_assoc. + rewrite <- Rinv_l_sym. + rewrite Rmult_1_r. + rewrite (Rmult_comm 2). + repeat rewrite Rmult_assoc. + rewrite <- Rinv_l_sym. + rewrite Rmult_1_r. + rewrite (Rmult_comm (/ 2)). + rewrite (Rmult_comm 2). + repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym. + rewrite Rmult_1_r. + rewrite (Rmult_comm a). + repeat rewrite Rmult_assoc. + rewrite <- Rinv_l_sym. + rewrite Rmult_1_r. + rewrite (Rmult_comm 2). + repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym. + rewrite Rmult_1_r. + repeat rewrite Rplus_assoc. + rewrite (Rplus_comm (Rsqr b * (Rsqr (/ a * / 2) * a))). + repeat rewrite Rplus_assoc. + rewrite (Rmult_comm x). + apply Rplus_eq_compat_l. + rewrite (Rmult_comm (/ a)). + unfold Rsqr in |- *; repeat rewrite Rmult_assoc. + rewrite <- Rinv_l_sym. + rewrite Rmult_1_r. + ring. + apply (cond_nonzero a). + discrR. + apply (cond_nonzero a). + discrR. + discrR. + apply (cond_nonzero a). + discrR. + discrR. + discrR. + apply (cond_nonzero a). + discrR. + apply (cond_nonzero a). Qed. Lemma Rsqr_eq : forall x y:R, Rsqr x = Rsqr y -> x = y \/ x = - y. -intros; unfold Rsqr in H; - generalize (Rplus_eq_compat_l (- (y * y)) (x * x) (y * y) H); - rewrite Rplus_opp_l; replace (- (y * y) + x * x) with ((x - y) * (x + y)). -intro; generalize (Rmult_integral (x - y) (x + y) H0); intro; elim H1; intros. -left; apply Rminus_diag_uniq; assumption. -right; apply Rminus_diag_uniq; unfold Rminus in |- *; rewrite Ropp_involutive; - assumption. -ring. -Qed.
\ No newline at end of file +Proof. + intros; unfold Rsqr in H; + generalize (Rplus_eq_compat_l (- (y * y)) (x * x) (y * y) H); + rewrite Rplus_opp_l; replace (- (y * y) + x * x) with ((x - y) * (x + y)). + intro; generalize (Rmult_integral (x - y) (x + y) H0); intro; elim H1; intros. + left; apply Rminus_diag_uniq; assumption. + right; apply Rminus_diag_uniq; unfold Rminus in |- *; rewrite Ropp_involutive; + assumption. + ring. +Qed. |