helm/software/matita/contribs/procedural/CoRN/transc/TrigMon.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "CoRN.ma".
  18
  19 (* $Id: TrigMon.v,v 1.9 2004/04/23 10:01:08 lcf Exp $ *)
  20
  21 include "transc/Pi.ma".
  22
  23 (* UNEXPORTED
  24 Opaque Sine Cosine.
  25 *)
  26
  27 (*#*
  28 Sign properties: cosine is positive in
  29 $(-\frac{\pi}2,\frac{\pi}2)$#(-&pi;/2,&pi;/2)#, sine in
  30 $(0,\pi)$#(0,&pi;)# and tangent in $(0,\frac{\pi}2)$#0,&pi;/2)#.
  31 *)
  32
  33 inline procedural "cic:/CoRN/transc/TrigMon/Cos_pos.con" as lemma.
  34
  35 inline procedural "cic:/CoRN/transc/TrigMon/Sin_pos.con" as lemma.
  36
  37 inline procedural "cic:/CoRN/transc/TrigMon/Tan_pos.con" as lemma.
  38
  39 inline procedural "cic:/CoRN/transc/TrigMon/Cos_nonneg.con" as lemma.
  40
  41 inline procedural "cic:/CoRN/transc/TrigMon/Sin_nonneg.con" as lemma.
  42
  43 (*#* Consequences. *)
  44
  45 inline procedural "cic:/CoRN/transc/TrigMon/Abs_Sin_less_One.con" as lemma.
  46
  47 inline procedural "cic:/CoRN/transc/TrigMon/Abs_Cos_less_One.con" as lemma.
  48
  49 (*#*
  50 Sine is (strictly) increasing in [[ [--]Pi[/]Two,Pi[/]Two]]; cosine
  51 is (strictly) decreasing in [[Zero,Pi]].
  52 *)
  53
  54 inline procedural "cic:/CoRN/transc/TrigMon/Sin_resp_leEq.con" as lemma.
  55
  56 inline procedural "cic:/CoRN/transc/TrigMon/Cos_resp_leEq.con" as lemma.
  57
  58 (* begin hide *)
  59
  60 inline procedural "cic:/CoRN/transc/TrigMon/Cos_resp_less_aux.con" as lemma.
  61
  62 inline procedural "cic:/CoRN/transc/TrigMon/Cos_resp_less_aux'.con" as lemma.
  63
  64 (* end hide *)
  65
  66 inline procedural "cic:/CoRN/transc/TrigMon/Cos_resp_less.con" as lemma.
  67
  68 inline procedural "cic:/CoRN/transc/TrigMon/Sin_resp_less.con" as lemma.
  69
  70 (* UNEXPORTED
  71 Section Tangent
  72 *)
  73
  74 (*#* **Derivative of Tangent
  75
  76 Finally, two formulas for the derivative of the tangent function and
  77 monotonicity properties.
  78 *)
  79
  80 inline procedural "cic:/CoRN/transc/TrigMon/bnd_Cos.con" as lemma.
  81
  82 (* UNEXPORTED
  83 Opaque Sine Cosine.
  84 *)
  85
  86 inline procedural "cic:/CoRN/transc/TrigMon/Derivative_Tan_1.con" as lemma.
  87
  88 inline procedural "cic:/CoRN/transc/TrigMon/Derivative_Tan_2.con" as lemma.
  89
  90 inline procedural "cic:/CoRN/transc/TrigMon/Tan_resp_less.con" as lemma.
  91
  92 inline procedural "cic:/CoRN/transc/TrigMon/Tan_resp_leEq.con" as lemma.
  93
  94 (* UNEXPORTED
  95 End Tangent
  96 *)
  97
  98 (* UNEXPORTED
  99 Hint Resolve Derivative_Tan_1 Derivative_Tan_2: derivate.
 100 *)
 101