← Back to branch summary

~ubuntu-branches/ubuntu/hardy/coq-doc/hardy

« back to all changes in this revision

Viewing changes to library/Coq.Reals.Rtrigo_calc.html

  • Committer: Bazaar Package Importer
  • Author(s): Samuel Mimram
  • Date: 2004-09-18 13:28:22 UTC
  • mfrom: (1.1.1 upstream)
  • Revision ID: james.westby@ubuntu.com-20040918132822-ees5mb8qmzd6a0fw
Tags: 8.0pl1.0-1
http://bugs.debian.org/272204
* Added the Coq faq, moved the tutorial to the root directory and added
  doc-base files for both, closes: #272204.
* Set dh_compat to level 4.

Show diffs side-by-side

added added

removed removed

Lines of Context:
library/Coq.Reals.Rtrigo_calc.html
 
1
<html xmlns="http://www.w3.org/1999/xhtml">
 
2
<head>
 
3
<meta http-equiv="Content-Type" content="text/html; charset="><link rel="stylesheet" href="style.css" type="text/css"><title>Coq.Reals.Rtrigo_calc</title>
 
4
</head>
 
5
 
 
6
<body>
 
7
 
 
8
<h1>Library Coq.Reals.Rtrigo_calc</h1>
 
9
 
 
10
<code>
 
11
<code class="keyword">Require</code> <code class="keyword">Import</code> Rbase.<br/>
 
12
<code class="keyword">Require</code> <code class="keyword">Import</code> Rfunctions.<br/>
 
13
<code class="keyword">Require</code> <code class="keyword">Import</code> SeqSeries.<br/>
 
14
<code class="keyword">Require</code> <code class="keyword">Import</code> Rtrigo.<br/>
 
15
<code class="keyword">Require</code> <code class="keyword">Import</code> R_sqrt.<br/>
 
16
Open <code class="keyword">Local</code> Scope R_scope.<br/>
 
17
 
 
18
<br/>
 
19
<code class="keyword">Lemma</code> <a name="tan_PI"></a>tan_PI : <a href="Coq.Reals.Rtrigo.html#tan">tan</a> <a href="Coq.Reals.AltSeries.html#PI">PI</a> = 0.<br/>
 
20
unfold tan in |- *; rewrite <a href="Coq.Reals.Rtrigo.html#sin_PI">sin_PI</a>; rewrite <a href="Coq.Reals.Rtrigo.html#cos_PI">cos_PI</a>; unfold Rdiv in |- *;<br/>
 
21
&nbsp;apply <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>. <br/>
 
22
<code class="keyword">Qed</code>.<br/>
 
23
 
 
24
<br/>
 
25
<code class="keyword">Lemma</code> <a name="sin_3PI2"></a>sin_3PI2 : <a href="Coq.Reals.Rtrigo_def.html#sin">sin</a> (3 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2)) = -1.<br/>
 
26
replace (3 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2)) with (<a href="Coq.Reals.AltSeries.html#PI">PI</a> + <a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2).<br/>
 
27
rewrite <a href="Coq.Reals.Rtrigo.html#sin_plus">sin_plus</a>; rewrite <a href="Coq.Reals.Rtrigo.html#sin_PI">sin_PI</a>; rewrite <a href="Coq.Reals.Rtrigo.html#cos_PI">cos_PI</a>; rewrite <a href="Coq.Reals.Rtrigo.html#sin_PI2">sin_PI2</a>; ring.<br/>
 
28
pattern <a href="Coq.Reals.AltSeries.html#PI">PI</a> at 1 in |- *; rewrite (<a href="Coq.Reals.RIneq.html#double_var">double_var</a> <a href="Coq.Reals.AltSeries.html#PI">PI</a>); ring.<br/>
 
29
<code class="keyword">Qed</code>.<br/>
 
30
 
 
31
<br/>
 
32
<code class="keyword">Lemma</code> <a name="tan_2PI"></a>tan_2PI : <a href="Coq.Reals.Rtrigo.html#tan">tan</a> (2 * <a href="Coq.Reals.AltSeries.html#PI">PI</a>) = 0.<br/>
 
33
unfold tan in |- *; rewrite <a href="Coq.Reals.Rtrigo.html#sin_2PI">sin_2PI</a>; unfold Rdiv in |- *; apply <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>.<br/>
 
34
<code class="keyword">Qed</code>.<br/>
 
35
 
 
36
<br/>
 
37
<code class="keyword">Lemma</code> <a name="sin_cos_PI4"></a>sin_cos_PI4 : <a href="Coq.Reals.Rtrigo_def.html#sin">sin</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4) = <a href="Coq.Reals.Rtrigo_def.html#cos">cos</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4).<br/>
 
38
<code class="keyword">Proof</code> with trivial.<br/>
 
39
rewrite <a href="Coq.Reals.Rtrigo.html#cos_sin">cos_sin</a>...<br/>
 
40
replace (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2 + <a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4) with (- (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4) + <a href="Coq.Reals.AltSeries.html#PI">PI</a>)...<br/>
 
41
rewrite <a href="Coq.Reals.Rtrigo.html#neg_sin">neg_sin</a>; rewrite <a href="Coq.Reals.Rtrigo.html#sin_neg">sin_neg</a>; ring...<br/>
 
42
cut (<a href="Coq.Reals.AltSeries.html#PI">PI</a> = <a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2 + <a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2); [ intro | apply double_var ]...<br/>
 
43
pattern <a href="Coq.Reals.AltSeries.html#PI">PI</a> at 2 3 in |- *; rewrite H; pattern <a href="Coq.Reals.AltSeries.html#PI">PI</a> at 2 3 in |- *; rewrite H...<br/>
 
44
assert (H0 : 2 &lt;&gt; 0);<br/>
 
45
&nbsp;[ discrR | unfold Rdiv in |- *; rewrite Rinv_mult_distr; try ring ]...<br/>
 
46
<code class="keyword">Qed</code>.<br/>
 
47
 
 
48
<br/>
 
49
<code class="keyword">Lemma</code> <a name="sin_PI3_cos_PI6"></a>sin_PI3_cos_PI6 : <a href="Coq.Reals.Rtrigo_def.html#sin">sin</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 3) = <a href="Coq.Reals.Rtrigo_def.html#cos">cos</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 6).<br/>
 
50
<code class="keyword">Proof</code> with trivial.<br/>
 
51
replace (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 6) with (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2 - <a href="Coq.Reals.AltSeries.html#PI">PI</a> / 3)...<br/>
 
52
rewrite <a href="Coq.Reals.Rtrigo.html#cos_shift">cos_shift</a>...<br/>
 
53
assert (H0 : 6 &lt;&gt; 0); [ discrR | idtac ]...<br/>
 
54
assert (H1 : 3 &lt;&gt; 0); [ discrR | idtac ]...<br/>
 
55
assert (H2 : 2 &lt;&gt; 0); [ discrR | idtac ]...<br/>
 
56
apply <a href="Coq.Reals.RIneq.html#Rmult_eq_reg_l">Rmult_eq_reg_l</a> with 6...<br/>
 
57
rewrite <a href="Coq.Reals.RIneq.html#Rmult_minus_distr_l">Rmult_minus_distr_l</a>; repeat rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> 6)...<br/>
 
58
unfold Rdiv in |- *; repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>...<br/>
 
59
rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_l_sym">Rinv_l_sym</a>...<br/>
 
60
rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (/ 3)); repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_r_sym">Rinv_r_sym</a>...<br/>
 
61
pattern <a href="Coq.Reals.AltSeries.html#PI">PI</a> at 2 in |- *; rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> <a href="Coq.Reals.AltSeries.html#PI">PI</a>); repeat rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>;<br/>
 
62
&nbsp;repeat rewrite &lt;- <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_l_sym">Rinv_l_sym</a>...<br/>
 
63
ring...<br/>
 
64
<code class="keyword">Qed</code>.<br/>
 
65
 
 
66
<br/>
 
67
<code class="keyword">Lemma</code> <a name="sin_PI6_cos_PI3"></a>sin_PI6_cos_PI3 : <a href="Coq.Reals.Rtrigo_def.html#cos">cos</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 3) = <a href="Coq.Reals.Rtrigo_def.html#sin">sin</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 6).<br/>
 
68
<code class="keyword">Proof</code> with trivial.<br/>
 
69
replace (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 6) with (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2 - <a href="Coq.Reals.AltSeries.html#PI">PI</a> / 3)...<br/>
 
70
rewrite <a href="Coq.Reals.Rtrigo.html#sin_shift">sin_shift</a>...<br/>
 
71
assert (H0 : 6 &lt;&gt; 0); [ discrR | idtac ]...<br/>
 
72
assert (H1 : 3 &lt;&gt; 0); [ discrR | idtac ]...<br/>
 
73
assert (H2 : 2 &lt;&gt; 0); [ discrR | idtac ]...<br/>
 
74
apply <a href="Coq.Reals.RIneq.html#Rmult_eq_reg_l">Rmult_eq_reg_l</a> with 6...<br/>
 
75
rewrite <a href="Coq.Reals.RIneq.html#Rmult_minus_distr_l">Rmult_minus_distr_l</a>; repeat rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> 6)...<br/>
 
76
unfold Rdiv in |- *; repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>...<br/>
 
77
rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_l_sym">Rinv_l_sym</a>...<br/>
 
78
rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (/ 3)); repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_r_sym">Rinv_r_sym</a>...<br/>
 
79
pattern <a href="Coq.Reals.AltSeries.html#PI">PI</a> at 2 in |- *; rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> <a href="Coq.Reals.AltSeries.html#PI">PI</a>); repeat rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>;<br/>
 
80
&nbsp;repeat rewrite &lt;- <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_l_sym">Rinv_l_sym</a>...<br/>
 
81
ring...<br/>
 
82
<code class="keyword">Qed</code>.<br/>
 
83
 
 
84
<br/>
 
85
<code class="keyword">Lemma</code> <a name="PI6_RGT_0"></a>PI6_RGT_0 : 0 &lt; <a href="Coq.Reals.AltSeries.html#PI">PI</a> / 6.<br/>
 
86
unfold Rdiv in |- *; apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>;<br/>
 
87
&nbsp;[ apply PI_RGT_0 | apply Rinv_0_lt_compat; prove_sup0 ].<br/>
 
88
<code class="keyword">Qed</code>.<br/>
 
89
 
 
90
<br/>
 
91
<code class="keyword">Lemma</code> <a name="PI6_RLT_PI2"></a>PI6_RLT_PI2 : <a href="Coq.Reals.AltSeries.html#PI">PI</a> / 6 &lt; <a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2.<br/>
 
92
unfold Rdiv in |- *; apply <a href="Coq.Reals.Raxioms.html#Rmult_lt_compat_l">Rmult_lt_compat_l</a>.<br/>
 
93
apply <a href="Coq.Reals.AltSeries.html#PI_RGT_0">PI_RGT_0</a>.<br/>
 
94
apply <a href="Coq.Reals.RIneq.html#Rinv_lt_contravar">Rinv_lt_contravar</a>; prove_sup.<br/>
 
95
<code class="keyword">Qed</code>.<br/>
 
96
 
 
97
<br/>
 
98
<code class="keyword">Lemma</code> <a name="sin_PI6"></a>sin_PI6 : <a href="Coq.Reals.Rtrigo_def.html#sin">sin</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 6) = 1 / 2.<br/>
 
99
<code class="keyword">Proof</code> with trivial.<br/>
 
100
assert (H : 2 &lt;&gt; 0); [ discrR | idtac ]...<br/>
 
101
apply <a href="Coq.Reals.RIneq.html#Rmult_eq_reg_l">Rmult_eq_reg_l</a> with (2 * <a href="Coq.Reals.Rtrigo_def.html#cos">cos</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 6))...<br/>
 
102
replace (2 * <a href="Coq.Reals.Rtrigo_def.html#cos">cos</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 6) * <a href="Coq.Reals.Rtrigo_def.html#sin">sin</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 6)) with<br/>
 
103
&nbsp;(2 * <a href="Coq.Reals.Rtrigo_def.html#sin">sin</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 6) * <a href="Coq.Reals.Rtrigo_def.html#cos">cos</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 6))...<br/>
 
104
rewrite &lt;- <a href="Coq.Reals.Rtrigo.html#sin_2a">sin_2a</a>; replace (2 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 6)) with (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 3)...<br/>
 
105
rewrite <a href="Coq.Reals.Rtrigo_calc.html#sin_PI3_cos_PI6">sin_PI3_cos_PI6</a>...<br/>
 
106
unfold Rdiv in |- *; rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>; rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>;<br/>
 
107
&nbsp;pattern 2 at 2 in |- *; rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> 2); rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>;<br/>
 
108
&nbsp;rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_l_sym">Rinv_l_sym</a>...<br/>
 
109
rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>...<br/>
 
110
unfold Rdiv in |- *; rewrite <a href="Coq.Reals.RIneq.html#Rinv_mult_distr">Rinv_mult_distr</a>...<br/>
 
111
rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (/ 2)); rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> 2);<br/>
 
112
&nbsp;repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_l_sym">Rinv_l_sym</a>...<br/>
 
113
rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>...<br/>
 
114
discrR...<br/>
 
115
ring...<br/>
 
116
apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>...<br/>
 
117
cut (0 &lt; <a href="Coq.Reals.Rtrigo_def.html#cos">cos</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 6));<br/>
 
118
&nbsp;[ intro H1; auto with real<br/>
 
119
&nbsp;| apply <a href="Coq.Reals.Rtrigo.html#cos_gt_0">cos_gt_0</a>;<br/>
 
120
&nbsp;&nbsp;&nbsp;&nbsp;[ apply (Rlt_trans (- (PI / 2)) 0 (PI / 6) _PI2_RLT_0 PI6_RGT_0)
 
121
    | apply PI6_RLT_PI2 ] ]...<br/>
 
122
<code class="keyword">Qed</code>.<br/>
 
123
 
 
124
<br/>
 
125
<code class="keyword">Lemma</code> <a name="sqrt2_neq_0"></a>sqrt2_neq_0 : <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 2 &lt;&gt; 0.<br/>
 
126
assert (Hyp : 0 &lt; 2);<br/>
 
127
&nbsp;[ prove_sup0<br/>
 
128
&nbsp;| generalize (<a href="Coq.Reals.RIneq.html#Rlt_le">Rlt_le</a> 0 2 Hyp); intro H1; red in |- *; intro H2;<br/>
 
129
&nbsp;&nbsp;&nbsp;&nbsp;generalize (<a href="Coq.Reals.R_sqrt.html#sqrt_eq_0">sqrt_eq_0</a> 2 H1 H2); intro H; absurd (2 = 0);<br/>
 
130
&nbsp;&nbsp;&nbsp;&nbsp;[ discrR | assumption ] ].<br/>
 
131
<code class="keyword">Qed</code>.<br/>
 
132
 
 
133
<br/>
 
134
<code class="keyword">Lemma</code> <a name="R1_sqrt2_neq_0"></a>R1_sqrt2_neq_0 : 1 / <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 2 &lt;&gt; 0.<br/>
 
135
generalize (<a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a> (<a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 2) <a href="Coq.Reals.Rtrigo_calc.html#sqrt2_neq_0">sqrt2_neq_0</a>); intro H;<br/>
 
136
&nbsp;generalize (<a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a> 1 (/ <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 2) <a href="Coq.Reals.Raxioms.html#R1_neq_R0">R1_neq_R0</a> H); <br/>
 
137
&nbsp;intro H0; assumption.<br/>
 
138
<code class="keyword">Qed</code>.<br/>
 
139
 
 
140
<br/>
 
141
<code class="keyword">Lemma</code> <a name="sqrt3_2_neq_0"></a>sqrt3_2_neq_0 : 2 * <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 3 &lt;&gt; 0.<br/>
 
142
apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>;<br/>
 
143
&nbsp;[ discrR<br/>
 
144
&nbsp;| assert (Hyp : 0 &lt; 3);<br/>
 
145
&nbsp;&nbsp;&nbsp;&nbsp;[ prove_sup0<br/>
 
146
&nbsp;&nbsp;&nbsp;&nbsp;| generalize (<a href="Coq.Reals.RIneq.html#Rlt_le">Rlt_le</a> 0 3 Hyp); intro H1; red in |- *; intro H2;<br/>
 
147
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;generalize (<a href="Coq.Reals.R_sqrt.html#sqrt_eq_0">sqrt_eq_0</a> 3 H1 H2); intro H; absurd (3 = 0);<br/>
 
148
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[ discrR | assumption ] ] ].<br/>
 
149
<code class="keyword">Qed</code>.<br/>
 
150
 
 
151
<br/>
 
152
<code class="keyword">Lemma</code> <a name="Rlt_sqrt2_0"></a>Rlt_sqrt2_0 : 0 &lt; <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 2.<br/>
 
153
assert (Hyp : 0 &lt; 2);<br/>
 
154
&nbsp;[ prove_sup0<br/>
 
155
&nbsp;| generalize (<a href="Coq.Reals.R_sqrt.html#sqrt_positivity">sqrt_positivity</a> 2 (<a href="Coq.Reals.RIneq.html#Rlt_le">Rlt_le</a> 0 2 Hyp)); intro H1; elim H1;<br/>
 
156
&nbsp;&nbsp;&nbsp;&nbsp;intro H2;<br/>
 
157
&nbsp;&nbsp;&nbsp;&nbsp;[ assumption<br/>
 
158
&nbsp;&nbsp;&nbsp;&nbsp;| absurd (0 = <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 2);<br/>
 
159
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[ apply (<a href="Coq.Init.Logic.html#sym_not_eq">sym_not_eq</a> (A:=<a href="Coq.Reals.Rdefinitions.html#R">R</a>)); apply <a href="Coq.Reals.Rtrigo_calc.html#sqrt2_neq_0">sqrt2_neq_0</a> | assumption ] ] ].<br/>
 
160
<code class="keyword">Qed</code>.<br/>
 
161
 
 
162
<br/>
 
163
<code class="keyword">Lemma</code> <a name="Rlt_sqrt3_0"></a>Rlt_sqrt3_0 : 0 &lt; <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 3.<br/>
 
164
cut (0%nat &lt;&gt; 1%nat);<br/>
 
165
&nbsp;[ intro H0; assert (Hyp : 0 &lt; 2);<br/>
 
166
&nbsp;&nbsp;&nbsp;&nbsp;[ prove_sup0<br/>
 
167
&nbsp;&nbsp;&nbsp;&nbsp;| generalize (<a href="Coq.Reals.RIneq.html#Rlt_le">Rlt_le</a> 0 2 Hyp); intro H1; assert (Hyp2 : 0 &lt; 3);<br/>
 
168
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[ prove_sup0<br/>
 
169
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| generalize (<a href="Coq.Reals.RIneq.html#Rlt_le">Rlt_le</a> 0 3 Hyp2); intro H2;<br/>
 
170
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;generalize (<a href="Coq.Reals.RIneq.html#lt_INR_0">lt_INR_0</a> 1 (<a href="Coq.Arith.Lt.html#neq_O_lt">neq_O_lt</a> 1 H0)); <br/>
 
171
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;unfold INR in |- *; intro H3;<br/>
 
172
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;generalize (<a href="Coq.Reals.Raxioms.html#Rplus_lt_compat_l">Rplus_lt_compat_l</a> 2 0 1 H3); <br/>
 
173
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;rewrite <a href="Coq.Reals.Raxioms.html#Rplus_comm">Rplus_comm</a>; rewrite <a href="Coq.Reals.Raxioms.html#Rplus_0_l">Rplus_0_l</a>; replace (2 + 1) with 3;<br/>
 
174
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[ intro H4; generalize (sqrt_lt_1 2 3 H1 H2 H4); clear H3; intro H3;
 
175
             apply (Rlt_trans 0 (sqrt 2) (sqrt 3) Rlt_sqrt2_0 H3)
 
176
          | ring ] ] ]<br/>
 
177
&nbsp;| discriminate ].<br/>
 
178
<code class="keyword">Qed</code>.<br/>
 
179
 
 
180
<br/>
 
181
<code class="keyword">Lemma</code> <a name="PI4_RGT_0"></a>PI4_RGT_0 : 0 &lt; <a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4.<br/>
 
182
unfold Rdiv in |- *; apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>;<br/>
 
183
&nbsp;[ apply PI_RGT_0 | apply Rinv_0_lt_compat; prove_sup0 ].<br/>
 
184
<code class="keyword">Qed</code>.<br/>
 
185
 
 
186
<br/>
 
187
<code class="keyword">Lemma</code> <a name="cos_PI4"></a>cos_PI4 : <a href="Coq.Reals.Rtrigo_def.html#cos">cos</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4) = 1 / <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 2.<br/>
 
188
<code class="keyword">Proof</code> with trivial.<br/>
 
189
apply <a href="Coq.Reals.R_sqr.html#Rsqr_inj">Rsqr_inj</a>...<br/>
 
190
apply <a href="Coq.Reals.Rtrigo.html#cos_ge_0">cos_ge_0</a>...<br/>
 
191
left; apply (<a href="Coq.Reals.Raxioms.html#Rlt_trans">Rlt_trans</a> (- (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2)) 0 (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4) <a href="Coq.Reals.Rtrigo.html#_PI2_RLT_0">_PI2_RLT_0</a> <a href="Coq.Reals.Rtrigo_calc.html#PI4_RGT_0">PI4_RGT_0</a>)...<br/>
 
192
left; apply <a href="Coq.Reals.Rtrigo.html#PI4_RLT_PI2">PI4_RLT_PI2</a>...<br/>
 
193
left; apply (<a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a> 1 (/ <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 2))...<br/>
 
194
prove_sup...<br/>
 
195
apply <a href="Coq.Reals.RIneq.html#Rinv_0_lt_compat">Rinv_0_lt_compat</a>; apply <a href="Coq.Reals.Rtrigo_calc.html#Rlt_sqrt2_0">Rlt_sqrt2_0</a>...<br/>
 
196
rewrite <a href="Coq.Reals.R_sqr.html#Rsqr_div">Rsqr_div</a>...<br/>
 
197
rewrite <a href="Coq.Reals.R_sqr.html#Rsqr_1">Rsqr_1</a>; rewrite <a href="Coq.Reals.R_sqrt.html#Rsqr_sqrt">Rsqr_sqrt</a>...<br/>
 
198
assert (H : 2 &lt;&gt; 0); [ discrR | idtac ]...<br/>
 
199
unfold Rsqr in |- *; pattern (<a href="Coq.Reals.Rtrigo_def.html#cos">cos</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4)) at 1 in |- *;<br/>
 
200
&nbsp;rewrite &lt;- <a href="Coq.Reals.Rtrigo_calc.html#sin_cos_PI4">sin_cos_PI4</a>;<br/>
 
201
&nbsp;replace (<a href="Coq.Reals.Rtrigo_def.html#sin">sin</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4) * <a href="Coq.Reals.Rtrigo_def.html#cos">cos</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4)) with<br/>
 
202
&nbsp;&nbsp;(1 / 2 * (2 * <a href="Coq.Reals.Rtrigo_def.html#sin">sin</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4) * <a href="Coq.Reals.Rtrigo_def.html#cos">cos</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4)))...<br/>
 
203
rewrite &lt;- <a href="Coq.Reals.Rtrigo.html#sin_2a">sin_2a</a>; replace (2 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4)) with (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2)...<br/>
 
204
rewrite <a href="Coq.Reals.Rtrigo.html#sin_PI2">sin_PI2</a>...<br/>
 
205
apply <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>...<br/>
 
206
unfold Rdiv in |- *; rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> 2); rewrite <a href="Coq.Reals.RIneq.html#Rinv_mult_distr">Rinv_mult_distr</a>...<br/>
 
207
repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_l_sym">Rinv_l_sym</a>...<br/>
 
208
rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>...<br/>
 
209
unfold Rdiv in |- *; rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>; repeat rewrite &lt;- <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>...<br/>
 
210
rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_l_sym">Rinv_l_sym</a>...<br/>
 
211
rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>...<br/>
 
212
left; prove_sup...<br/>
 
213
apply <a href="Coq.Reals.Rtrigo_calc.html#sqrt2_neq_0">sqrt2_neq_0</a>...<br/>
 
214
<code class="keyword">Qed</code>.<br/>
 
215
 
 
216
<br/>
 
217
<code class="keyword">Lemma</code> <a name="sin_PI4"></a>sin_PI4 : <a href="Coq.Reals.Rtrigo_def.html#sin">sin</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4) = 1 / <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 2.<br/>
 
218
rewrite <a href="Coq.Reals.Rtrigo_calc.html#sin_cos_PI4">sin_cos_PI4</a>; apply <a href="Coq.Reals.Rtrigo_calc.html#cos_PI4">cos_PI4</a>.<br/>
 
219
<code class="keyword">Qed</code>.<br/>
 
220
 
 
221
<br/>
 
222
<code class="keyword">Lemma</code> <a name="tan_PI4"></a>tan_PI4 : <a href="Coq.Reals.Rtrigo.html#tan">tan</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4) = 1.<br/>
 
223
unfold tan in |- *; rewrite <a href="Coq.Reals.Rtrigo_calc.html#sin_cos_PI4">sin_cos_PI4</a>.<br/>
 
224
unfold Rdiv in |- *; apply <a href="Coq.Reals.RIneq.html#Rinv_r">Rinv_r</a>.<br/>
 
225
change (<a href="Coq.Reals.Rtrigo_def.html#cos">cos</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4) &lt;&gt; 0) in |- *; rewrite <a href="Coq.Reals.Rtrigo_calc.html#cos_PI4">cos_PI4</a>; apply <a href="Coq.Reals.Rtrigo_calc.html#R1_sqrt2_neq_0">R1_sqrt2_neq_0</a>.<br/>
 
226
<code class="keyword">Qed</code>.<br/>
 
227
 
 
228
<br/>
 
229
<code class="keyword">Lemma</code> <a name="cos3PI4"></a>cos3PI4 : <a href="Coq.Reals.Rtrigo_def.html#cos">cos</a> (3 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4)) = -1 / <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 2.<br/>
 
230
<code class="keyword">Proof</code> with trivial.<br/>
 
231
replace (3 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4)) with (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2 - - (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4))...<br/>
 
232
rewrite <a href="Coq.Reals.Rtrigo.html#cos_shift">cos_shift</a>; rewrite <a href="Coq.Reals.Rtrigo.html#sin_neg">sin_neg</a>; rewrite <a href="Coq.Reals.Rtrigo_calc.html#sin_PI4">sin_PI4</a>...<br/>
 
233
unfold Rdiv in |- *; rewrite <a href="Coq.Reals.RIneq.html#Ropp_mult_distr_l_reverse">Ropp_mult_distr_l_reverse</a>...<br/>
 
234
unfold Rminus in |- *; rewrite <a href="Coq.Reals.RIneq.html#Ropp_involutive">Ropp_involutive</a>; pattern <a href="Coq.Reals.AltSeries.html#PI">PI</a> at 1 in |- *;<br/>
 
235
&nbsp;rewrite <a href="Coq.Reals.RIneq.html#double_var">double_var</a>; unfold Rdiv in |- *; rewrite <a href="Coq.Reals.RIneq.html#Rmult_plus_distr_r">Rmult_plus_distr_r</a>;<br/>
 
236
&nbsp;repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_mult_distr">Rinv_mult_distr</a>;<br/>
 
237
&nbsp;[ ring | discrR | discrR ]...<br/>
 
238
<code class="keyword">Qed</code>.<br/>
 
239
 
 
240
<br/>
 
241
<code class="keyword">Lemma</code> <a name="sin3PI4"></a>sin3PI4 : <a href="Coq.Reals.Rtrigo_def.html#sin">sin</a> (3 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4)) = 1 / <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 2.<br/>
 
242
<code class="keyword">Proof</code> with trivial.<br/>
 
243
replace (3 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4)) with (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2 - - (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4))...<br/>
 
244
rewrite <a href="Coq.Reals.Rtrigo.html#sin_shift">sin_shift</a>; rewrite <a href="Coq.Reals.Rtrigo.html#cos_neg">cos_neg</a>; rewrite <a href="Coq.Reals.Rtrigo_calc.html#cos_PI4">cos_PI4</a>...<br/>
 
245
unfold Rminus in |- *; rewrite <a href="Coq.Reals.RIneq.html#Ropp_involutive">Ropp_involutive</a>; pattern <a href="Coq.Reals.AltSeries.html#PI">PI</a> at 1 in |- *;<br/>
 
246
&nbsp;rewrite <a href="Coq.Reals.RIneq.html#double_var">double_var</a>; unfold Rdiv in |- *; rewrite <a href="Coq.Reals.RIneq.html#Rmult_plus_distr_r">Rmult_plus_distr_r</a>;<br/>
 
247
&nbsp;repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_mult_distr">Rinv_mult_distr</a>;<br/>
 
248
&nbsp;[ ring | discrR | discrR ]...<br/>
 
249
<code class="keyword">Qed</code>.<br/>
 
250
 
 
251
<br/>
 
252
<code class="keyword">Lemma</code> <a name="cos_PI6"></a>cos_PI6 : <a href="Coq.Reals.Rtrigo_def.html#cos">cos</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 6) = <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 3 / 2.<br/>
 
253
<code class="keyword">Proof</code> with trivial.<br/>
 
254
apply <a href="Coq.Reals.R_sqr.html#Rsqr_inj">Rsqr_inj</a>...<br/>
 
255
apply <a href="Coq.Reals.Rtrigo.html#cos_ge_0">cos_ge_0</a>...<br/>
 
256
left; apply (<a href="Coq.Reals.Raxioms.html#Rlt_trans">Rlt_trans</a> (- (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2)) 0 (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 6) <a href="Coq.Reals.Rtrigo.html#_PI2_RLT_0">_PI2_RLT_0</a> <a href="Coq.Reals.Rtrigo_calc.html#PI6_RGT_0">PI6_RGT_0</a>)...<br/>
 
257
left; apply <a href="Coq.Reals.Rtrigo_calc.html#PI6_RLT_PI2">PI6_RLT_PI2</a>...<br/>
 
258
left; apply (<a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a> (<a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 3) (/ 2))...<br/>
 
259
apply <a href="Coq.Reals.Rtrigo_calc.html#Rlt_sqrt3_0">Rlt_sqrt3_0</a>...<br/>
 
260
apply <a href="Coq.Reals.RIneq.html#Rinv_0_lt_compat">Rinv_0_lt_compat</a>; prove_sup0...<br/>
 
261
assert (H : 2 &lt;&gt; 0); [ discrR | idtac ]...<br/>
 
262
assert (H1 : 4 &lt;&gt; 0); [ apply prod_neq_R0 | idtac ]...<br/>
 
263
rewrite <a href="Coq.Reals.R_sqr.html#Rsqr_div">Rsqr_div</a>...<br/>
 
264
rewrite <a href="Coq.Reals.Rtrigo.html#cos2">cos2</a>; unfold Rsqr in |- *; rewrite <a href="Coq.Reals.Rtrigo_calc.html#sin_PI6">sin_PI6</a>; rewrite <a href="Coq.Reals.R_sqrt.html#sqrt_def">sqrt_def</a>...<br/>
 
265
unfold Rdiv in |- *; rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>; apply <a href="Coq.Reals.RIneq.html#Rmult_eq_reg_l">Rmult_eq_reg_l</a> with 4...<br/>
 
266
rewrite <a href="Coq.Reals.RIneq.html#Rmult_minus_distr_l">Rmult_minus_distr_l</a>; rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> 3);<br/>
 
267
&nbsp;repeat rewrite &lt;- <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_r_sym">Rinv_r_sym</a>...<br/>
 
268
rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>; rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>...<br/>
 
269
rewrite &lt;- (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (/ 2)); repeat rewrite &lt;- <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>...<br/>
 
270
rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_l_sym">Rinv_l_sym</a>...<br/>
 
271
rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>; rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_r_sym">Rinv_r_sym</a>...<br/>
 
272
ring...<br/>
 
273
left; prove_sup0...<br/>
 
274
<code class="keyword">Qed</code>.<br/>
 
275
 
 
276
<br/>
 
277
<code class="keyword">Lemma</code> <a name="tan_PI6"></a>tan_PI6 : <a href="Coq.Reals.Rtrigo.html#tan">tan</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 6) = 1 / <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 3.<br/>
 
278
unfold tan in |- *; rewrite <a href="Coq.Reals.Rtrigo_calc.html#sin_PI6">sin_PI6</a>; rewrite <a href="Coq.Reals.Rtrigo_calc.html#cos_PI6">cos_PI6</a>; unfold Rdiv in |- *;<br/>
 
279
&nbsp;repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>; rewrite <a href="Coq.Reals.RIneq.html#Rinv_mult_distr">Rinv_mult_distr</a>.<br/>
 
280
rewrite <a href="Coq.Reals.RIneq.html#Rinv_involutive">Rinv_involutive</a>.<br/>
 
281
rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (/ 2)); rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_r_sym">Rinv_r_sym</a>.<br/>
 
282
apply <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>.<br/>
 
283
discrR.<br/>
 
284
discrR.<br/>
 
285
red in |- *; intro; assert (H1:= <a href="Coq.Reals.Rtrigo_calc.html#Rlt_sqrt3_0">Rlt_sqrt3_0</a>); rewrite H in H1;<br/>
 
286
&nbsp;elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> 0 H1).<br/>
 
287
apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; discrR.<br/>
 
288
<code class="keyword">Qed</code>.<br/>
 
289
 
 
290
<br/>
 
291
<code class="keyword">Lemma</code> <a name="sin_PI3"></a>sin_PI3 : <a href="Coq.Reals.Rtrigo_def.html#sin">sin</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 3) = <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 3 / 2.<br/>
 
292
rewrite <a href="Coq.Reals.Rtrigo_calc.html#sin_PI3_cos_PI6">sin_PI3_cos_PI6</a>; apply <a href="Coq.Reals.Rtrigo_calc.html#cos_PI6">cos_PI6</a>.<br/>
 
293
<code class="keyword">Qed</code>.<br/>
 
294
 
 
295
<br/>
 
296
<code class="keyword">Lemma</code> <a name="cos_PI3"></a>cos_PI3 : <a href="Coq.Reals.Rtrigo_def.html#cos">cos</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 3) = 1 / 2.<br/>
 
297
rewrite <a href="Coq.Reals.Rtrigo_calc.html#sin_PI6_cos_PI3">sin_PI6_cos_PI3</a>; apply <a href="Coq.Reals.Rtrigo_calc.html#sin_PI6">sin_PI6</a>.<br/>
 
298
<code class="keyword">Qed</code>.<br/>
 
299
 
 
300
<br/>
 
301
<code class="keyword">Lemma</code> <a name="tan_PI3"></a>tan_PI3 : <a href="Coq.Reals.Rtrigo.html#tan">tan</a> (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 3) = <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 3.<br/>
 
302
unfold tan in |- *; rewrite <a href="Coq.Reals.Rtrigo_calc.html#sin_PI3">sin_PI3</a>; rewrite <a href="Coq.Reals.Rtrigo_calc.html#cos_PI3">cos_PI3</a>; unfold Rdiv in |- *;<br/>
 
303
&nbsp;rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>; rewrite <a href="Coq.Reals.RIneq.html#Rinv_involutive">Rinv_involutive</a>.<br/>
 
304
rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_l_sym">Rinv_l_sym</a>.<br/>
 
305
apply <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>.<br/>
 
306
discrR.<br/>
 
307
discrR.<br/>
 
308
<code class="keyword">Qed</code>.<br/>
 
309
 
 
310
<br/>
 
311
<code class="keyword">Lemma</code> <a name="sin_2PI3"></a>sin_2PI3 : <a href="Coq.Reals.Rtrigo_def.html#sin">sin</a> (2 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 3)) = <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 3 / 2.<br/>
 
312
rewrite <a href="Coq.Reals.RIneq.html#double">double</a>; rewrite <a href="Coq.Reals.Rtrigo.html#sin_plus">sin_plus</a>; rewrite <a href="Coq.Reals.Rtrigo_calc.html#sin_PI3">sin_PI3</a>; rewrite <a href="Coq.Reals.Rtrigo_calc.html#cos_PI3">cos_PI3</a>;<br/>
 
313
&nbsp;unfold Rdiv in |- *; repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>; rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (/ 2));<br/>
 
314
&nbsp;repeat rewrite &lt;- <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; rewrite <a href="Coq.Reals.RIneq.html#double_var">double_var</a>; <br/>
 
315
&nbsp;reflexivity.<br/>
 
316
<code class="keyword">Qed</code>.<br/>
 
317
 
 
318
<br/>
 
319
<code class="keyword">Lemma</code> <a name="cos_2PI3"></a>cos_2PI3 : <a href="Coq.Reals.Rtrigo_def.html#cos">cos</a> (2 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 3)) = -1 / 2.<br/>
 
320
<code class="keyword">Proof</code> with trivial.<br/>
 
321
assert (H : 2 &lt;&gt; 0); [ discrR | idtac ]...<br/>
 
322
assert (H0 : 4 &lt;&gt; 0); [ apply prod_neq_R0 | idtac ]...<br/>
 
323
rewrite <a href="Coq.Reals.RIneq.html#double">double</a>; rewrite <a href="Coq.Reals.Cos_plus.html#cos_plus">cos_plus</a>; rewrite <a href="Coq.Reals.Rtrigo_calc.html#sin_PI3">sin_PI3</a>; rewrite <a href="Coq.Reals.Rtrigo_calc.html#cos_PI3">cos_PI3</a>;<br/>
 
324
&nbsp;unfold Rdiv in |- *; rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>; apply <a href="Coq.Reals.RIneq.html#Rmult_eq_reg_l">Rmult_eq_reg_l</a> with 4...<br/>
 
325
rewrite <a href="Coq.Reals.RIneq.html#Rmult_minus_distr_l">Rmult_minus_distr_l</a>; repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>;<br/>
 
326
&nbsp;rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> 2)...<br/>
 
327
repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_l_sym">Rinv_l_sym</a>...<br/>
 
328
rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>; rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_r_sym">Rinv_r_sym</a>...<br/>
 
329
pattern 2 at 4 in |- *; rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> 2); repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>;<br/>
 
330
&nbsp;rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_l_sym">Rinv_l_sym</a>...<br/>
 
331
rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>; rewrite <a href="Coq.Reals.RIneq.html#Ropp_mult_distr_r_reverse">Ropp_mult_distr_r_reverse</a>; rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>...<br/>
 
332
rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> 2); repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_l_sym">Rinv_l_sym</a>...<br/>
 
333
rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>; rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> 2); rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (/ 2))...<br/>
 
334
repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_l_sym">Rinv_l_sym</a>...<br/>
 
335
rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>; rewrite <a href="Coq.Reals.R_sqrt.html#sqrt_def">sqrt_def</a>...<br/>
 
336
ring...<br/>
 
337
left; prove_sup...<br/>
 
338
<code class="keyword">Qed</code>.<br/>
 
339
 
 
340
<br/>
 
341
<code class="keyword">Lemma</code> <a name="tan_2PI3"></a>tan_2PI3 : <a href="Coq.Reals.Rtrigo.html#tan">tan</a> (2 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 3)) = - <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 3.<br/>
 
342
<code class="keyword">Proof</code> with trivial.<br/>
 
343
assert (H : 2 &lt;&gt; 0); [ discrR | idtac ]...<br/>
 
344
unfold tan in |- *; rewrite <a href="Coq.Reals.Rtrigo_calc.html#sin_2PI3">sin_2PI3</a>; rewrite <a href="Coq.Reals.Rtrigo_calc.html#cos_2PI3">cos_2PI3</a>; unfold Rdiv in |- *;<br/>
 
345
&nbsp;rewrite <a href="Coq.Reals.RIneq.html#Ropp_mult_distr_l_reverse">Ropp_mult_distr_l_reverse</a>; rewrite <a href="Coq.Reals.Raxioms.html#Rmult_1_l">Rmult_1_l</a>;<br/>
 
346
&nbsp;rewrite &lt;- <a href="Coq.Reals.RIneq.html#Ropp_inv_permute">Ropp_inv_permute</a>...<br/>
 
347
rewrite <a href="Coq.Reals.RIneq.html#Rinv_involutive">Rinv_involutive</a>...<br/>
 
348
rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>; rewrite <a href="Coq.Reals.RIneq.html#Ropp_mult_distr_r_reverse">Ropp_mult_distr_r_reverse</a>; rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_l_sym">Rinv_l_sym</a>...<br/>
 
349
ring...<br/>
 
350
apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>...<br/>
 
351
<code class="keyword">Qed</code>.<br/>
 
352
 
 
353
<br/>
 
354
<code class="keyword">Lemma</code> <a name="cos_5PI4"></a>cos_5PI4 : <a href="Coq.Reals.Rtrigo_def.html#cos">cos</a> (5 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4)) = -1 / <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 2.<br/>
 
355
<code class="keyword">Proof</code> with trivial.<br/>
 
356
replace (5 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4)) with (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4 + <a href="Coq.Reals.AltSeries.html#PI">PI</a>)...<br/>
 
357
rewrite <a href="Coq.Reals.Rtrigo.html#neg_cos">neg_cos</a>; rewrite <a href="Coq.Reals.Rtrigo_calc.html#cos_PI4">cos_PI4</a>; unfold Rdiv in |- *;<br/>
 
358
&nbsp;rewrite <a href="Coq.Reals.RIneq.html#Ropp_mult_distr_l_reverse">Ropp_mult_distr_l_reverse</a>...<br/>
 
359
pattern <a href="Coq.Reals.AltSeries.html#PI">PI</a> at 2 in |- *; rewrite <a href="Coq.Reals.RIneq.html#double_var">double_var</a>; pattern <a href="Coq.Reals.AltSeries.html#PI">PI</a> at 2 3 in |- *;<br/>
 
360
&nbsp;rewrite <a href="Coq.Reals.RIneq.html#double_var">double_var</a>; assert (H : 2 &lt;&gt; 0);<br/>
 
361
&nbsp;[ discrR | unfold Rdiv in |- *; repeat rewrite Rinv_mult_distr; try ring ]...<br/>
 
362
<code class="keyword">Qed</code>.<br/>
 
363
 
 
364
<br/>
 
365
<code class="keyword">Lemma</code> <a name="sin_5PI4"></a>sin_5PI4 : <a href="Coq.Reals.Rtrigo_def.html#sin">sin</a> (5 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4)) = -1 / <a href="Coq.Reals.R_sqrt.html#sqrt">sqrt</a> 2.<br/>
 
366
<code class="keyword">Proof</code> with trivial.<br/>
 
367
replace (5 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4)) with (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4 + <a href="Coq.Reals.AltSeries.html#PI">PI</a>)...<br/>
 
368
rewrite <a href="Coq.Reals.Rtrigo.html#neg_sin">neg_sin</a>; rewrite <a href="Coq.Reals.Rtrigo_calc.html#sin_PI4">sin_PI4</a>; unfold Rdiv in |- *;<br/>
 
369
&nbsp;rewrite <a href="Coq.Reals.RIneq.html#Ropp_mult_distr_l_reverse">Ropp_mult_distr_l_reverse</a>...<br/>
 
370
pattern <a href="Coq.Reals.AltSeries.html#PI">PI</a> at 2 in |- *; rewrite <a href="Coq.Reals.RIneq.html#double_var">double_var</a>; pattern <a href="Coq.Reals.AltSeries.html#PI">PI</a> at 2 3 in |- *;<br/>
 
371
&nbsp;rewrite <a href="Coq.Reals.RIneq.html#double_var">double_var</a>; assert (H : 2 &lt;&gt; 0);<br/>
 
372
&nbsp;[ discrR | unfold Rdiv in |- *; repeat rewrite Rinv_mult_distr; try ring ]...<br/>
 
373
<code class="keyword">Qed</code>.<br/>
 
374
 
 
375
<br/>
 
376
<code class="keyword">Lemma</code> <a name="sin_cos5PI4"></a>sin_cos5PI4 : <a href="Coq.Reals.Rtrigo_def.html#cos">cos</a> (5 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4)) = <a href="Coq.Reals.Rtrigo_def.html#sin">sin</a> (5 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 4)).<br/>
 
377
rewrite <a href="Coq.Reals.Rtrigo_calc.html#cos_5PI4">cos_5PI4</a>; rewrite <a href="Coq.Reals.Rtrigo_calc.html#sin_5PI4">sin_5PI4</a>; reflexivity.<br/>
 
378
<code class="keyword">Qed</code>.<br/>
 
379
 
 
380
<br/>
 
381
<code class="keyword">Lemma</code> <a name="Rgt_3PI2_0"></a>Rgt_3PI2_0 : 0 &lt; 3 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2).<br/>
 
382
apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>;<br/>
 
383
&nbsp;[ prove_sup0<br/>
 
384
&nbsp;| unfold Rdiv in |- *; apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>;<br/>
 
385
&nbsp;&nbsp;&nbsp;&nbsp;[ apply PI_RGT_0 | apply Rinv_0_lt_compat; prove_sup0 ] ].<br/>
 
386
<code class="keyword">Qed</code>.<br/>
 
387
 
 
388
<br/>
 
389
<code class="keyword">Lemma</code> <a name="Rgt_2PI_0"></a>Rgt_2PI_0 : 0 &lt; 2 * <a href="Coq.Reals.AltSeries.html#PI">PI</a>.<br/>
 
390
apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>; [ prove_sup0 | apply PI_RGT_0 ].<br/>
 
391
<code class="keyword">Qed</code>.<br/>
 
392
 
 
393
<br/>
 
394
<code class="keyword">Lemma</code> <a name="Rlt_PI_3PI2"></a>Rlt_PI_3PI2 : <a href="Coq.Reals.AltSeries.html#PI">PI</a> &lt; 3 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2).<br/>
 
395
generalize <a href="Coq.Reals.Rtrigo.html#PI2_RGT_0">PI2_RGT_0</a>; intro H1;<br/>
 
396
&nbsp;generalize (<a href="Coq.Reals.Raxioms.html#Rplus_lt_compat_l">Rplus_lt_compat_l</a> <a href="Coq.Reals.AltSeries.html#PI">PI</a> 0 (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2) H1);<br/>
 
397
&nbsp;replace (<a href="Coq.Reals.AltSeries.html#PI">PI</a> + <a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2) with (3 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2)).<br/>
 
398
rewrite <a href="Coq.Reals.RIneq.html#Rplus_0_r">Rplus_0_r</a>; intro H2; assumption.<br/>
 
399
pattern <a href="Coq.Reals.AltSeries.html#PI">PI</a> at 2 in |- *; rewrite <a href="Coq.Reals.RIneq.html#double_var">double_var</a>; ring.<br/>
 
400
<code class="keyword">Qed</code>. <br/>
 
401
&nbsp;<br/>
 
402
<code class="keyword">Lemma</code> <a name="Rlt_3PI2_2PI"></a>Rlt_3PI2_2PI : 3 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2) &lt; 2 * <a href="Coq.Reals.AltSeries.html#PI">PI</a>.<br/>
 
403
generalize <a href="Coq.Reals.Rtrigo.html#PI2_RGT_0">PI2_RGT_0</a>; intro H1;<br/>
 
404
&nbsp;generalize (<a href="Coq.Reals.Raxioms.html#Rplus_lt_compat_l">Rplus_lt_compat_l</a> (3 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2)) 0 (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2) H1);<br/>
 
405
&nbsp;replace (3 * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2) + <a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2) with (2 * <a href="Coq.Reals.AltSeries.html#PI">PI</a>).<br/>
 
406
rewrite <a href="Coq.Reals.RIneq.html#Rplus_0_r">Rplus_0_r</a>; intro H2; assumption.<br/>
 
407
rewrite <a href="Coq.Reals.RIneq.html#double">double</a>; pattern <a href="Coq.Reals.AltSeries.html#PI">PI</a> at 1 2 in |- *; rewrite <a href="Coq.Reals.RIneq.html#double_var">double_var</a>; ring.<br/>
 
408
<code class="keyword">Qed</code>.<br/>
 
409
 
 
410
<br/>
 
411
<code class="keyword">Definition</code> <a name="plat"></a>plat : <a href="Coq.Reals.Rdefinitions.html#R">R</a> := 180.<br/>
 
412
<code class="keyword">Definition</code> <a name="toRad"></a>toRad (x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>) : <a href="Coq.Reals.Rdefinitions.html#R">R</a> := x * <a href="Coq.Reals.AltSeries.html#PI">PI</a> * / <a href="Coq.Reals.Rtrigo_calc.html#plat">plat</a>.<br/>
 
413
<code class="keyword">Definition</code> <a name="toDeg"></a>toDeg (x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>) : <a href="Coq.Reals.Rdefinitions.html#R">R</a> := x * <a href="Coq.Reals.Rtrigo_calc.html#plat">plat</a> * / <a href="Coq.Reals.AltSeries.html#PI">PI</a>.<br/>
 
414
 
 
415
<br/>
 
416
<code class="keyword">Lemma</code> <a name="rad_deg"></a>rad_deg : forall x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, <a href="Coq.Reals.Rtrigo_calc.html#toRad">toRad</a> (<a href="Coq.Reals.Rtrigo_calc.html#toDeg">toDeg</a> x) = x.<br/>
 
417
intro; unfold toRad, toDeg in |- *;<br/>
 
418
&nbsp;replace (x * <a href="Coq.Reals.Rtrigo_calc.html#plat">plat</a> * / <a href="Coq.Reals.AltSeries.html#PI">PI</a> * <a href="Coq.Reals.AltSeries.html#PI">PI</a> * / <a href="Coq.Reals.Rtrigo_calc.html#plat">plat</a>) with<br/>
 
419
&nbsp;&nbsp;(x * (<a href="Coq.Reals.Rtrigo_calc.html#plat">plat</a> * / <a href="Coq.Reals.Rtrigo_calc.html#plat">plat</a>) * (<a href="Coq.Reals.AltSeries.html#PI">PI</a> * / <a href="Coq.Reals.AltSeries.html#PI">PI</a>)); [ idtac | ring ].<br/>
 
420
repeat rewrite &lt;- <a href="Coq.Reals.RIneq.html#Rinv_r_sym">Rinv_r_sym</a>.<br/>
 
421
ring.<br/>
 
422
apply <a href="Coq.Reals.Rtrigo.html#PI_neq0">PI_neq0</a>.<br/>
 
423
unfold plat in |- *; discrR.<br/>
 
424
<code class="keyword">Qed</code>.<br/>
 
425
 
 
426
<br/>
 
427
<code class="keyword">Lemma</code> <a name="toRad_inj"></a>toRad_inj : forall x y:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, <a href="Coq.Reals.Rtrigo_calc.html#toRad">toRad</a> x = <a href="Coq.Reals.Rtrigo_calc.html#toRad">toRad</a> y -&gt; x = y.<br/>
 
428
intros; unfold toRad in H; apply <a href="Coq.Reals.RIneq.html#Rmult_eq_reg_l">Rmult_eq_reg_l</a> with <a href="Coq.Reals.AltSeries.html#PI">PI</a>.<br/>
 
429
rewrite &lt;- (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> x); rewrite &lt;- (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> y).<br/>
 
430
apply <a href="Coq.Reals.RIneq.html#Rmult_eq_reg_l">Rmult_eq_reg_l</a> with (/ <a href="Coq.Reals.Rtrigo_calc.html#plat">plat</a>).<br/>
 
431
rewrite &lt;- (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (x * <a href="Coq.Reals.AltSeries.html#PI">PI</a>)); rewrite &lt;- (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (y * <a href="Coq.Reals.AltSeries.html#PI">PI</a>));<br/>
 
432
&nbsp;assumption.<br/>
 
433
apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; unfold plat in |- *; discrR.<br/>
 
434
apply <a href="Coq.Reals.Rtrigo.html#PI_neq0">PI_neq0</a>.<br/>
 
435
<code class="keyword">Qed</code>.<br/>
 
436
 
 
437
<br/>
 
438
<code class="keyword">Lemma</code> <a name="deg_rad"></a>deg_rad : forall x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, <a href="Coq.Reals.Rtrigo_calc.html#toDeg">toDeg</a> (<a href="Coq.Reals.Rtrigo_calc.html#toRad">toRad</a> x) = x.<br/>
 
439
intro x; apply <a href="Coq.Reals.Rtrigo_calc.html#toRad_inj">toRad_inj</a>; rewrite (<a href="Coq.Reals.Rtrigo_calc.html#rad_deg">rad_deg</a> (<a href="Coq.Reals.Rtrigo_calc.html#toRad">toRad</a> x)); reflexivity.<br/>
 
440
<code class="keyword">Qed</code>.<br/>
 
441
 
 
442
<br/>
 
443
<code class="keyword">Definition</code> <a name="sind"></a>sind (x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>) : <a href="Coq.Reals.Rdefinitions.html#R">R</a> := <a href="Coq.Reals.Rtrigo_def.html#sin">sin</a> (<a href="Coq.Reals.Rtrigo_calc.html#toRad">toRad</a> x).<br/>
 
444
<code class="keyword">Definition</code> <a name="cosd"></a>cosd (x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>) : <a href="Coq.Reals.Rdefinitions.html#R">R</a> := <a href="Coq.Reals.Rtrigo_def.html#cos">cos</a> (<a href="Coq.Reals.Rtrigo_calc.html#toRad">toRad</a> x).<br/>
 
445
<code class="keyword">Definition</code> <a name="tand"></a>tand (x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>) : <a href="Coq.Reals.Rdefinitions.html#R">R</a> := <a href="Coq.Reals.Rtrigo.html#tan">tan</a> (<a href="Coq.Reals.Rtrigo_calc.html#toRad">toRad</a> x).<br/>
 
446
 
 
447
<br/>
 
448
<code class="keyword">Lemma</code> <a name="Rsqr_sin_cos_d_one"></a>Rsqr_sin_cos_d_one : forall x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, <a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (<a href="Coq.Reals.Rtrigo_calc.html#sind">sind</a> x) + <a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (<a href="Coq.Reals.Rtrigo_calc.html#cosd">cosd</a> x) = 1.<br/>
 
449
intro x; unfold sind in |- *; unfold cosd in |- *; apply <a href="Coq.Reals.Rtrigo.html#sin2_cos2">sin2_cos2</a>.<br/>
 
450
<code class="keyword">Qed</code>.<br/>
 
451
 
 
452
<br/>
 
453
<code class="keyword">Lemma</code> <a name="sin_lb_ge_0"></a>sin_lb_ge_0 : forall a:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, 0 &lt;= a -&gt; a &lt;= <a href="Coq.Reals.AltSeries.html#PI">PI</a> / 2 -&gt; 0 &lt;= <a href="Coq.Reals.Rtrigo.html#sin_lb">sin_lb</a> a.<br/>
 
454
intros; case (<a href="Coq.Reals.RIneq.html#Rtotal_order">Rtotal_order</a> 0 a); intro.<br/>
 
455
left; apply <a href="Coq.Reals.Rtrigo.html#sin_lb_gt_0">sin_lb_gt_0</a>; assumption.<br/>
 
456
elim H1; intro.<br/>
 
457
rewrite &lt;- H2; unfold sin_lb in |- *; unfold sin_approx in |- *;<br/>
 
458
&nbsp;unfold sum_f_R0 in |- *; unfold sin_term in |- *; <br/>
 
459
&nbsp;repeat rewrite <a href="Coq.Reals.Rfunctions.html#pow_ne_zero">pow_ne_zero</a>.<br/>
 
460
unfold Rdiv in |- *; repeat rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>; repeat rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_r">Rmult_0_r</a>;<br/>
 
461
&nbsp;repeat rewrite <a href="Coq.Reals.RIneq.html#Rplus_0_r">Rplus_0_r</a>; right; reflexivity.<br/>
 
462
discriminate.<br/>
 
463
discriminate.<br/>
 
464
discriminate.<br/>
 
465
discriminate.<br/>
 
466
elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> 0 (<a href="Coq.Reals.RIneq.html#Rle_lt_trans">Rle_lt_trans</a> 0 a 0 H H2)).<br/>
 
467
<code class="keyword">Qed</code>.</code>
 
468
<hr/><a href="index.html">Index</a><hr/><font size="-1">This page has been generated by <a href="http://www.lri.fr/~filliatr/coqdoc/">coqdoc</a></font>
 
469
</body>
 
470
</html>
 
 
b'\\ No newline at end of file'