Rtrigo_calc.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Import Rtrigo1.
Require Import R_sqrt.
Local Open Scope R_scope.

Lemma tan_PI : tan PI = 0.tan PI = 0
Proof.tan PI = 0
  unfold tan; rewrite sin_PI; rewrite cos_PI; unfold Rdiv;
    apply Rmult_0_l.
Qed.

Lemma sin_3PI2 : sin (3 * (PI / 2)) = -1.sin (3 * (PI / 2)) = -1
Proof.sin (3 * (PI / 2)) = -1
  replace (3 * (PI / 2)) with (PI + PI / 2).sin (PI + PI / 2) = -1
PI + PI / 2 = 3 * (PI / 2)
  rewrite sin_plus; rewrite sin_PI; rewrite cos_PI; rewrite sin_PI2; ring.PI + PI / 2 = 3 * (PI / 2)
  pattern PI at 1; rewrite (double_var PI); ring.
Qed.

Lemma tan_2PI : tan (2 * PI) = 0.tan (2 * PI) = 0
Proof.tan (2 * PI) = 0
  unfold tan; rewrite sin_2PI; unfold Rdiv; apply Rmult_0_l.
Qed.

Lemma sin_cos_PI4 : sin (PI / 4) = cos (PI / 4).sin (PI / 4) = cos (PI / 4)
Proof.sin (PI / 4) = cos (PI / 4)
  rewrite cos_sin.sin (PI / 4) = sin (PI / 2 + PI / 4)
  replace (PI / 2 + PI / 4) with (- (PI / 4) + PI) by field.sin (PI / 4) = sin (- (PI / 4) + PI)
  rewrite neg_sin, sin_neg; ring.
Qed.

Lemma sin_PI3_cos_PI6 : sin (PI / 3) = cos (PI / 6).sin (PI / 3) = cos (PI / 6)
Proof.sin (PI / 3) = cos (PI / 6)
  replace (PI / 6) with (PI / 2 - PI / 3) by field.sin (PI / 3) = cos (PI / 2 - PI / 3)
  now rewrite cos_shift.
Qed.

Lemma sin_PI6_cos_PI3 : cos (PI / 3) = sin (PI / 6).cos (PI / 3) = sin (PI / 6)
Proof.cos (PI / 3) = sin (PI / 6)
  replace (PI / 6) with (PI / 2 - PI / 3) by field.cos (PI / 3) = sin (PI / 2 - PI / 3)
  now rewrite sin_shift.
Qed.

Lemma PI6_RGT_0 : 0 < PI / 6.0 < PI / 6
Proof.0 < PI / 6
  unfold Rdiv; apply Rmult_lt_0_compat;
    [ apply PI_RGT_0 | apply Rinv_0_lt_compat; prove_sup0 ].
Qed.

Lemma PI6_RLT_PI2 : PI / 6 < PI / 2.PI / 6 < PI / 2
Proof.PI / 6 < PI / 2
  unfold Rdiv; apply Rmult_lt_compat_l.0 < PI
/ 6 < / 2
  apply PI_RGT_0./ 6 < / 2
  apply Rinv_lt_contravar; prove_sup.
Qed.

Lemma sin_PI6 : sin (PI / 6) = 1 / 2.sin (PI / 6) = 1 / 2
Proof.sin (PI / 6) = 1 / 2
  apply Rmult_eq_reg_l with (2 * cos (PI / 6)).2 * cos (PI / 6) * sin (PI / 6) =
2 * cos (PI / 6) * (1 / 2)
2 * cos (PI / 6) <> 0
  replace (2 * cos (PI / 6) * sin (PI / 6)) with
  (2 * sin (PI / 6) * cos (PI / 6)) by ring.2 * sin (PI / 6) * cos (PI / 6) =
2 * cos (PI / 6) * (1 / 2)
2 * cos (PI / 6) <> 0
  rewrite <- sin_2a; replace (2 * (PI / 6)) with (PI / 3) by field.sin (PI / 3) = 2 * cos (PI / 6) * (1 / 2)
2 * cos (PI / 6) <> 0
  rewrite sin_PI3_cos_PI6.cos (PI / 6) = 2 * cos (PI / 6) * (1 / 2)
2 * cos (PI / 6) <> 0
  field.2 * cos (PI / 6) <> 0
  apply prod_neq_R0.2 <> 0
cos (PI / 6) <> 0
  discrR.cos (PI / 6) <> 0
  cut (0 < cos (PI / 6));
    [ intro H1; auto with real
      | apply cos_gt_0;
        [ apply (Rlt_trans (- (PI / 2)) 0 (PI / 6) _PI2_RLT_0 PI6_RGT_0)
          | apply PI6_RLT_PI2 ] ].
Qed.

Lemma sqrt2_neq_0 : sqrt 2 <> 0.sqrt 2 <> 0
Proof.sqrt 2 <> 0
  assert (Hyp : 0 < 2);
    [ prove_sup0
      | generalize (Rlt_le 0 2 Hyp); intro H1; red; intro H2;
        generalize (sqrt_eq_0 2 H1 H2); intro H; absurd (2 = 0);
          [ discrR | assumption ] ].
Qed.

Lemma R1_sqrt2_neq_0 : 1 / sqrt 2 <> 0.1 / sqrt 2 <> 0
Proof.1 / sqrt 2 <> 0
  generalize (Rinv_neq_0_compat (sqrt 2) sqrt2_neq_0); intro H;
    generalize (prod_neq_R0 1 (/ sqrt 2) R1_neq_R0 H);
      intro H0; assumption.
Qed.

Lemma sqrt3_2_neq_0 : 2 * sqrt 3 <> 0.2 * sqrt 3 <> 0
Proof.2 * sqrt 3 <> 0
  apply prod_neq_R0;
    [ discrR
      | assert (Hyp : 0 < 3);
        [ prove_sup0
          | generalize (Rlt_le 0 3 Hyp); intro H1; red; intro H2;
            generalize (sqrt_eq_0 3 H1 H2); intro H; absurd (3 = 0);
              [ discrR | assumption ] ] ].
Qed.

Lemma Rlt_sqrt2_0 : 0 < sqrt 2.0 < sqrt 2
Proof.0 < sqrt 2
  assert (Hyp : 0 < 2);
    [ prove_sup0
      | generalize (sqrt_positivity 2 (Rlt_le 0 2 Hyp)); intro H1; elim H1;
        intro H2;
          [ assumption
            | absurd (0 = sqrt 2);
              [ apply (not_eq_sym (A:=R)); apply sqrt2_neq_0 | assumption ] ] ].
Qed.

Lemma Rlt_sqrt3_0 : 0 < sqrt 3.0 < sqrt 3
Proof.0 < sqrt 3
  cut (0%nat <> 1%nat);
    [ intro H0; assert (Hyp : 0 < 2);
      [ prove_sup0
        | generalize (Rlt_le 0 2 Hyp); intro H1; assert (Hyp2 : 0 < 3);
          [ prove_sup0
            | generalize (Rlt_le 0 3 Hyp2); intro H2;
              generalize (lt_INR_0 1 (neq_O_lt 1 H0));
                unfold INR; intro H3;
                  generalize (Rplus_lt_compat_l 2 0 1 H3);
                    rewrite Rplus_comm; rewrite Rplus_0_l; replace (2 + 1) with 3;
                      [ intro H4; generalize (sqrt_lt_1 2 3 H1 H2 H4); clear H3; intro H3;
                        apply (Rlt_trans 0 (sqrt 2) (sqrt 3) Rlt_sqrt2_0 H3)
                        | ring ] ] ]
      | discriminate ].
Qed.

Lemma PI4_RGT_0 : 0 < PI / 4.0 < PI / 4
Proof.0 < PI / 4
  unfold Rdiv; apply Rmult_lt_0_compat;
    [ apply PI_RGT_0 | apply Rinv_0_lt_compat; prove_sup0 ].
Qed.

Lemma cos_PI4 : cos (PI / 4) = 1 / sqrt 2.cos (PI / 4) = 1 / sqrt 2
Proof with trivial.cos (PI / 4) = 1 / sqrt 2
  apply Rsqr_inj...0 <= cos (PI / 4)
0 <= 1 / sqrt 2
(cos (PI / 4))² = (1 / sqrt 2)²
  apply cos_ge_0...- (PI / 2) <= PI / 4
PI / 4 <= PI / 2
0 <= 1 / sqrt 2
(cos (PI / 4))² = (1 / sqrt 2)²
  left; apply (Rlt_trans (- (PI / 2)) 0 (PI / 4) _PI2_RLT_0 PI4_RGT_0)...PI / 4 <= PI / 2
0 <= 1 / sqrt 2
(cos (PI / 4))² = (1 / sqrt 2)²
  left; apply PI4_RLT_PI2...0 <= 1 / sqrt 2
(cos (PI / 4))² = (1 / sqrt 2)²
  left; apply (Rmult_lt_0_compat 1 (/ sqrt 2))...0 < 1
0 < / sqrt 2
(cos (PI / 4))² = (1 / sqrt 2)²
  prove_sup...0 < / sqrt 2
(cos (PI / 4))² = (1 / sqrt 2)²
  apply Rinv_0_lt_compat; apply Rlt_sqrt2_0...(cos (PI / 4))² = (1 / sqrt 2)²
  rewrite Rsqr_div...(cos (PI / 4))² = 1² / (sqrt 2)²
sqrt 2 <> 0
  rewrite Rsqr_1; rewrite Rsqr_sqrt...(cos (PI / 4))² = 1 / 2
0 <= 2
sqrt 2 <> 0
  unfold Rsqr; pattern (cos (PI / 4)) at 1;
    rewrite <- sin_cos_PI4;
      replace (sin (PI / 4) * cos (PI / 4)) with
      (1 / 2 * (2 * sin (PI / 4) * cos (PI / 4))) by field.1 / 2 * (2 * sin (PI / 4) * cos (PI / 4)) = 1 / 2
0 <= 2
sqrt 2 <> 0
  rewrite <- sin_2a; replace (2 * (PI / 4)) with (PI / 2) by field.1 / 2 * sin (PI / 2) = 1 / 2
0 <= 2
sqrt 2 <> 0
  rewrite sin_PI2...1 / 2 * 1 = 1 / 2
0 <= 2
sqrt 2 <> 0
  field.0 <= 2
sqrt 2 <> 0
  left; prove_sup...sqrt 2 <> 0
  apply sqrt2_neq_0...
Qed.

Lemma sin_PI4 : sin (PI / 4) = 1 / sqrt 2.sin (PI / 4) = 1 / sqrt 2
Proof.sin (PI / 4) = 1 / sqrt 2
  rewrite sin_cos_PI4; apply cos_PI4.
Qed.

Lemma tan_PI4 : tan (PI / 4) = 1.tan (PI / 4) = 1
Proof.tan (PI / 4) = 1
  unfold tan; rewrite sin_cos_PI4.cos (PI / 4) / cos (PI / 4) = 1
  unfold Rdiv; apply Rinv_r.cos (PI * / 4) <> 0
  change (cos (PI / 4) <> 0); rewrite cos_PI4; apply R1_sqrt2_neq_0.
Qed.

Lemma cos_3PI4 : cos (3 * (PI / 4)) = -1 / sqrt 2.cos (3 * (PI / 4)) = -1 / sqrt 2
Proof.cos (3 * (PI / 4)) = -1 / sqrt 2
  replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field.cos (PI / 2 - - (PI / 4)) = -1 / sqrt 2
  rewrite cos_shift; rewrite sin_neg; rewrite sin_PI4.- (1 / sqrt 2) = -1 / sqrt 2
  unfold Rdiv.- (1 * / sqrt 2) = -1 * / sqrt 2
  ring.
Qed.

Notation cos3PI4 := cos_3PI4 (compat "8.10").

Lemma sin_3PI4 : sin (3 * (PI / 4)) = 1 / sqrt 2.sin (3 * (PI / 4)) = 1 / sqrt 2
Proof.sin (3 * (PI / 4)) = 1 / sqrt 2
  replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field.sin (PI / 2 - - (PI / 4)) = 1 / sqrt 2
  now rewrite sin_shift, cos_neg, cos_PI4.
Qed.

Notation sin3PI4 := sin_3PI4 (compat "8.10").

Lemma cos_PI6 : cos (PI / 6) = sqrt 3 / 2.cos (PI / 6) = sqrt 3 / 2
Proof with trivial.cos (PI / 6) = sqrt 3 / 2
  apply Rsqr_inj...0 <= cos (PI / 6)
0 <= sqrt 3 / 2
(cos (PI / 6))² = (sqrt 3 / 2)²
  apply cos_ge_0...- (PI / 2) <= PI / 6
PI / 6 <= PI / 2
0 <= sqrt 3 / 2
(cos (PI / 6))² = (sqrt 3 / 2)²
  left; apply (Rlt_trans (- (PI / 2)) 0 (PI / 6) _PI2_RLT_0 PI6_RGT_0)...PI / 6 <= PI / 2
0 <= sqrt 3 / 2
(cos (PI / 6))² = (sqrt 3 / 2)²
  left; apply PI6_RLT_PI2...0 <= sqrt 3 / 2
(cos (PI / 6))² = (sqrt 3 / 2)²
  left; apply (Rmult_lt_0_compat (sqrt 3) (/ 2))...0 < sqrt 3
0 < / 2
(cos (PI / 6))² = (sqrt 3 / 2)²
  apply Rlt_sqrt3_0...0 < / 2
(cos (PI / 6))² = (sqrt 3 / 2)²
  apply Rinv_0_lt_compat; prove_sup0...(cos (PI / 6))² = (sqrt 3 / 2)²
  rewrite Rsqr_div...(cos (PI / 6))² = (sqrt 3)² / 2²
  rewrite cos2; unfold Rsqr; rewrite sin_PI6; rewrite sqrt_def...1 - 1 / 2 * (1 / 2) = 3 / (2 * 2)
0 <= 3
  field.0 <= 3
  left ; prove_sup0.
Qed.

Lemma tan_PI6 : tan (PI / 6) = 1 / sqrt 3.tan (PI / 6) = 1 / sqrt 3
Proof.tan (PI / 6) = 1 / sqrt 3
  unfold tan; rewrite sin_PI6; rewrite cos_PI6; unfold Rdiv;
    repeat rewrite Rmult_1_l; rewrite Rinv_mult_distr./ 2 * (/ sqrt 3 * / / 2) = / sqrt 3
sqrt 3 <> 0
/ 2 <> 0
  rewrite Rinv_involutive./ 2 * (/ sqrt 3 * 2) = / sqrt 3
2 <> 0
sqrt 3 <> 0
/ 2 <> 0
  rewrite (Rmult_comm (/ 2)); rewrite Rmult_assoc; rewrite <- Rinv_r_sym./ sqrt 3 * 1 = / sqrt 3
2 <> 0
2 <> 0
sqrt 3 <> 0
/ 2 <> 0
  apply Rmult_1_r.2 <> 0
2 <> 0
sqrt 3 <> 0
/ 2 <> 0
  discrR.2 <> 0
sqrt 3 <> 0
/ 2 <> 0
  discrR.sqrt 3 <> 0
/ 2 <> 0
  red; intro; assert (H1 := Rlt_sqrt3_0); rewrite H in H1;
    elim (Rlt_irrefl 0 H1)./ 2 <> 0
  apply Rinv_neq_0_compat; discrR.
Qed.

Lemma sin_PI3 : sin (PI / 3) = sqrt 3 / 2.sin (PI / 3) = sqrt 3 / 2
Proof.sin (PI / 3) = sqrt 3 / 2
  rewrite sin_PI3_cos_PI6; apply cos_PI6.
Qed.

Lemma cos_PI3 : cos (PI / 3) = 1 / 2.cos (PI / 3) = 1 / 2
Proof.cos (PI / 3) = 1 / 2
  rewrite sin_PI6_cos_PI3; apply sin_PI6.
Qed.

Lemma tan_PI3 : tan (PI / 3) = sqrt 3.tan (PI / 3) = sqrt 3
Proof.tan (PI / 3) = sqrt 3
  unfold tan; rewrite sin_PI3; rewrite cos_PI3; unfold Rdiv;
    rewrite Rmult_1_l; rewrite Rinv_involutive.sqrt 3 * / 2 * 2 = sqrt 3
2 <> 0
  rewrite Rmult_assoc; rewrite <- Rinv_l_sym.sqrt 3 * 1 = sqrt 3
2 <> 0
2 <> 0
  apply Rmult_1_r.2 <> 0
2 <> 0
  discrR.2 <> 0
  discrR.
Qed.

Lemma sin_2PI3 : sin (2 * (PI / 3)) = sqrt 3 / 2.sin (2 * (PI / 3)) = sqrt 3 / 2
Proof.sin (2 * (PI / 3)) = sqrt 3 / 2
  rewrite double; rewrite sin_plus; rewrite sin_PI3; rewrite cos_PI3;
    unfold Rdiv; repeat rewrite Rmult_1_l; rewrite (Rmult_comm (/ 2));
      repeat rewrite <- Rmult_assoc; rewrite double_var;
        reflexivity.
Qed.

Lemma cos_2PI3 : cos (2 * (PI / 3)) = -1 / 2.cos (2 * (PI / 3)) = -1 / 2
Proof.cos (2 * (PI / 3)) = -1 / 2
  rewrite cos_2a, sin_PI3, cos_PI3.1 / 2 * (1 / 2) - sqrt 3 / 2 * (sqrt 3 / 2) = -1 / 2
  replace (sqrt 3 / 2 * (sqrt 3 / 2)) with ((sqrt 3 * sqrt 3) / 4) by field.1 / 2 * (1 / 2) - sqrt 3 * sqrt 3 / 4 = -1 / 2
  rewrite sqrt_sqrt.1 / 2 * (1 / 2) - 3 / 4 = -1 / 2
0 <= 3
  field.0 <= 3
  left ; prove_sup0.
Qed.

Lemma tan_2PI3 : tan (2 * (PI / 3)) = - sqrt 3.tan (2 * (PI / 3)) = - sqrt 3
Proof.tan (2 * (PI / 3)) = - sqrt 3
  unfold tan; rewrite sin_2PI3, cos_2PI3.sqrt 3 / 2 / (-1 / 2) = - sqrt 3
  field.
Qed.

Lemma cos_5PI4 : cos (5 * (PI / 4)) = -1 / sqrt 2.cos (5 * (PI / 4)) = -1 / sqrt 2
Proof.cos (5 * (PI / 4)) = -1 / sqrt 2
  replace (5 * (PI / 4)) with (PI / 4 + PI) by field.cos (PI / 4 + PI) = -1 / sqrt 2
  rewrite neg_cos; rewrite cos_PI4; unfold Rdiv.- (1 * / sqrt 2) = -1 * / sqrt 2
  ring.
Qed.

Lemma sin_5PI4 : sin (5 * (PI / 4)) = -1 / sqrt 2.sin (5 * (PI / 4)) = -1 / sqrt 2
Proof.sin (5 * (PI / 4)) = -1 / sqrt 2
  replace (5 * (PI / 4)) with (PI / 4 + PI) by field.sin (PI / 4 + PI) = -1 / sqrt 2
  rewrite neg_sin; rewrite sin_PI4; unfold Rdiv.- (1 * / sqrt 2) = -1 * / sqrt 2
  ring.
Qed.

Lemma sin_cos5PI4 : cos (5 * (PI / 4)) = sin (5 * (PI / 4)).cos (5 * (PI / 4)) = sin (5 * (PI / 4))
Proof.cos (5 * (PI / 4)) = sin (5 * (PI / 4))
  rewrite cos_5PI4; rewrite sin_5PI4; reflexivity.
Qed.

Lemma Rgt_3PI2_0 : 0 < 3 * (PI / 2).0 < 3 * (PI / 2)
Proof.0 < 3 * (PI / 2)
  apply Rmult_lt_0_compat;
    [ prove_sup0
      | unfold Rdiv; apply Rmult_lt_0_compat;
        [ apply PI_RGT_0 | apply Rinv_0_lt_compat; prove_sup0 ] ].
Qed.

Lemma Rgt_2PI_0 : 0 < 2 * PI.0 < 2 * PI
Proof.0 < 2 * PI
  apply Rmult_lt_0_compat; [ prove_sup0 | apply PI_RGT_0 ].
Qed.

Lemma Rlt_PI_3PI2 : PI < 3 * (PI / 2).PI < 3 * (PI / 2)
Proof.PI < 3 * (PI / 2)
  generalize PI2_RGT_0; intro H1;
    generalize (Rplus_lt_compat_l PI 0 (PI / 2) H1);
      replace (PI + PI / 2) with (3 * (PI / 2)).H1:0 < PI / 2
PI + 0 < 3 * (PI / 2) -> PI < 3 * (PI / 2)
H1:0 < PI / 2
3 * (PI / 2) = PI + PI / 2
  rewrite Rplus_0_r; intro H2; assumption.H1:0 < PI / 2
3 * (PI / 2) = PI + PI / 2
  pattern PI at 2; rewrite double_var; ring.
Qed.

Lemma Rlt_3PI2_2PI : 3 * (PI / 2) < 2 * PI.3 * (PI / 2) < 2 * PI
Proof.3 * (PI / 2) < 2 * PI
  generalize PI2_RGT_0; intro H1;
    generalize (Rplus_lt_compat_l (3 * (PI / 2)) 0 (PI / 2) H1);
      replace (3 * (PI / 2) + PI / 2) with (2 * PI).H1:0 < PI / 2
3 * (PI / 2) + 0 < 2 * PI -> 3 * (PI / 2) < 2 * PI
H1:0 < PI / 2
2 * PI = 3 * (PI / 2) + PI / 2
  rewrite Rplus_0_r; intro H2; assumption.H1:0 < PI / 2
2 * PI = 3 * (PI / 2) + PI / 2
  rewrite double; pattern PI at 1 2; rewrite double_var; ring.
Qed.

(***************************************************************)

Radian -> Degree | Degree -> Radian

(***************************************************************)

Definition plat : R := 180.
Definition toRad (x:R) : R := x * PI * / plat.
Definition toDeg (x:R) : R := x * plat * / PI.

Lemma rad_deg : forall x:R, toRad (toDeg x) = x.forall x : R, toRad (toDeg x) = x
Proof.forall x : R, toRad (toDeg x) = x
  intro; unfold toRad, toDeg;
    replace (x * plat * / PI * PI * / plat) with
    (x * (plat * / plat) * (PI * / PI)); [ idtac | ring ].x:R
x * (plat * / plat) * (PI * / PI) = x
  repeat rewrite <- Rinv_r_sym.x:R
x * 1 * 1 = x
x:R
PI <> 0
x:R
plat <> 0
  ring.x:R
PI <> 0
x:R
plat <> 0
  apply PI_neq0.x:R
plat <> 0
  unfold plat; discrR.
Qed.

Lemma toRad_inj : forall x y:R, toRad x = toRad y -> x = y.forall x y : R, toRad x = toRad y -> x = y
Proof.forall x y : R, toRad x = toRad y -> x = y
  intros; unfold toRad in H; apply Rmult_eq_reg_l with PI.x, y:R
H:x * PI * / plat = y * PI * / plat
PI * x = PI * y
x, y:R
H:x * PI * / plat = y * PI * / plat
PI <> 0
  rewrite <- (Rmult_comm x); rewrite <- (Rmult_comm y).x, y:R
H:x * PI * / plat = y * PI * / plat
x * PI = y * PI
x, y:R
H:x * PI * / plat = y * PI * / plat
PI <> 0
  apply Rmult_eq_reg_l with (/ plat).x, y:R
H:x * PI * / plat = y * PI * / plat
/ plat * (x * PI) = / plat * (y * PI)
x, y:R
H:x * PI * / plat = y * PI * / plat
/ plat <> 0
x, y:R
H:x * PI * / plat = y * PI * / plat
PI <> 0
  rewrite <- (Rmult_comm (x * PI)); rewrite <- (Rmult_comm (y * PI));
    assumption.x, y:R
H:x * PI * / plat = y * PI * / plat
/ plat <> 0
x, y:R
H:x * PI * / plat = y * PI * / plat
PI <> 0
  apply Rinv_neq_0_compat; unfold plat; discrR.x, y:R
H:x * PI * / plat = y * PI * / plat
PI <> 0
  apply PI_neq0.
Qed.

Lemma deg_rad : forall x:R, toDeg (toRad x) = x.forall x : R, toDeg (toRad x) = x
Proof.forall x : R, toDeg (toRad x) = x
  intro x; apply toRad_inj; rewrite (rad_deg (toRad x)); reflexivity.
Qed.

Definition sind (x:R) : R := sin (toRad x).
Definition cosd (x:R) : R := cos (toRad x).
Definition tand (x:R) : R := tan (toRad x).

Lemma Rsqr_sin_cos_d_one : forall x:R, Rsqr (sind x) + Rsqr (cosd x) = 1.forall x : R, (sind x)² + (cosd x)² = 1
Proof.forall x : R, (sind x)² + (cosd x)² = 1
  intro x; unfold sind; unfold cosd; apply sin2_cos2.
Qed.

(***************************************************)

Other properties

(***************************************************)

Lemma sin_lb_ge_0 : forall a:R, 0 <= a -> a <= PI / 2 -> 0 <= sin_lb a.forall a : R, 0 <= a -> a <= PI / 2 -> 0 <= sin_lb a
Proof.forall a : R, 0 <= a -> a <= PI / 2 -> 0 <= sin_lb a
  intros; case (Rtotal_order 0 a); intro.a:R
H:0 <= a
H0:a <= PI / 2
H1:0 < a
0 <= sin_lb a
a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
0 <= sin_lb a
  left; apply sin_lb_gt_0; assumption.a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
0 <= sin_lb a
  elim H1; intro.a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 = a
0 <= sin_lb a
a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 > a
0 <= sin_lb a
  rewrite <- H2; unfold sin_lb; unfold sin_approx;
    unfold sum_f_R0; unfold sin_term;
      repeat rewrite pow_ne_zero.a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 = a
0 <=
(-1) ^ 0 * (0 / INR (fact (2 * 0 + 1))) +
(-1) ^ 1 * (0 / INR (fact (2 * 1 + 1))) +
(-1) ^ 2 * (0 / INR (fact (2 * 2 + 1))) +
(-1) ^ 3 * (0 / INR (fact (2 * 3 + 1)))
a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 = a
(2 * 3 + 1)%nat <> 0%nat
a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 = a
(2 * 2 + 1)%nat <> 0%nat
a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 = a
(2 * 1 + 1)%nat <> 0%nat
a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 = a
(2 * 0 + 1)%nat <> 0%nat
a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 > a
0 <= sin_lb a
  unfold Rdiv; repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r;
    repeat rewrite Rplus_0_r; right; reflexivity.a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 = a
(2 * 3 + 1)%nat <> 0%nat
a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 = a
(2 * 2 + 1)%nat <> 0%nat
a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 = a
(2 * 1 + 1)%nat <> 0%nat
a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 = a
(2 * 0 + 1)%nat <> 0%nat
a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 > a
0 <= sin_lb a
  discriminate.a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 = a
(2 * 2 + 1)%nat <> 0%nat
a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 = a
(2 * 1 + 1)%nat <> 0%nat
a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 = a
(2 * 0 + 1)%nat <> 0%nat
a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 > a
0 <= sin_lb a
  discriminate.a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 = a
(2 * 1 + 1)%nat <> 0%nat
a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 = a
(2 * 0 + 1)%nat <> 0%nat
a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 > a
0 <= sin_lb a
  discriminate.a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 = a
(2 * 0 + 1)%nat <> 0%nat
a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 > a
0 <= sin_lb a
  discriminate.a:R
H:0 <= a
H0:a <= PI / 2
H1:0 = a \/ 0 > a
H2:0 > a
0 <= sin_lb a
  elim (Rlt_irrefl 0 (Rle_lt_trans 0 a 0 H H2)).
Qed.