blob: eaa0690cb6b589e6223e322093cd75676d231bcf (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
|
Require Reals.
Axiom y : R->R.
Axiom d_y : (derivable y).
Axiom n_y : (x:R)``(y x)<>0``.
Axiom dy_0 : (derive_pt y R0 (d_y R0)) == R1.
Lemma essai0 : (continuity_pt [x:R]``(x+2)/(y x)+x/(y x)`` R0).
Assert H := d_y.
Assert H0 := n_y.
Reg.
Qed.
Lemma essai1 : (derivable_pt [x:R]``/2*(sin x)`` ``1``).
Reg.
Qed.
Lemma essai2 : (continuity [x:R]``(Rsqr x)*(cos (x*x))+x``).
Reg.
Qed.
Lemma essai3 : (derivable_pt [x:R]``x*((Rsqr x)+3)`` R0).
Reg.
Qed.
Lemma essai4 : (derivable [x:R]``(x+x)*(sin x)``).
Reg.
Qed.
Lemma essai5 : (derivable [x:R]``1+(sin (2*x+3))*(cos (cos x))``).
Reg.
Qed.
Lemma essai6 : (derivable [x:R]``(cos (x+3))``).
Reg.
Qed.
Lemma essai7 : (derivable_pt [x:R]``(cos (/(sqrt x)))*(Rsqr ((sin x)+1))`` R1).
Reg.
Apply Rlt_R0_R1.
Red; Intro; Rewrite sqrt_1 in H; Assert H0 := R1_neq_R0; Elim H0; Assumption.
Qed.
Lemma essai8 : (derivable_pt [x:R]``(sqrt ((Rsqr x)+(sin x)+1))`` R0).
Reg.
Rewrite sin_0.
Rewrite Rsqr_O.
Replace ``0+0+1`` with ``1``; [Apply Rlt_R0_R1 | Ring].
Qed.
Lemma essai9 : (derivable_pt (plus_fct id sin) R1).
Reg.
Qed.
Lemma essai10 : (derivable_pt [x:R]``x+2`` R0).
Reg.
Qed.
Lemma essai11 : (derive_pt [x:R]``x+2`` R0 essai10)==R1.
Reg.
Qed.
Lemma essai12 : (derivable [x:R]``x+(Rsqr (x+2))``).
Reg.
Qed.
Lemma essai13 : (derive_pt [x:R]``x+(Rsqr (x+2))`` R0 (essai12 R0)) == ``5``.
Reg.
Qed.
Lemma essai14 : (derivable_pt [x:R]``2*x+x`` ``2``).
Reg.
Qed.
Lemma essai15 : (derive_pt [x:R]``2*x+x`` ``2`` essai14) == ``3``.
Reg.
Qed.
Lemma essai16 : (derivable_pt [x:R]``x+(sin x)`` R0).
Reg.
Qed.
Lemma essai17 : (derive_pt [x:R]``x+(sin x)`` R0 essai16)==``2``.
Reg.
Rewrite cos_0.
Reflexivity.
Qed.
Lemma essai18 : (derivable_pt [x:R]``x+(y x)`` ``0``).
Assert H := d_y.
Reg.
Qed.
Lemma essai19 : (derive_pt [x:R]``x+(y x)`` ``0`` essai18) == ``2``.
Assert H := dy_0.
Assert H0 := d_y.
Reg.
Qed.
Axiom z:R->R.
Axiom d_z: (derivable z).
Lemma essai20 : (derivable_pt [x:R]``(z (y x))`` R0).
Reg.
Apply d_y.
Apply d_z.
Qed.
Lemma essai21 : (derive_pt [x:R]``(z (y x))`` R0 essai20) == R1.
Assert H := dy_0.
Reg.
Abort.
Lemma essai22 : (derivable [x:R]``(sin (z x))+(Rsqr (z x))/(y x)``).
Assert H := d_y.
Reg.
Apply n_y.
Apply d_z.
Qed.
(* Pour tester la continuite de sqrt en 0 *)
Lemma essai23 : (continuity_pt [x:R]``(sin (sqrt (x-1)))+(exp (Rsqr ((sqrt x)+3)))`` R1).
Reg.
Left; Apply Rlt_R0_R1.
Right; Unfold Rminus; Rewrite Rplus_Ropp_r; Reflexivity.
Qed.
Lemma essai24 : (derivable [x:R]``(sqrt (x*x+2*x+2))+(Rabsolu (x*x+1))``).
Reg.
Replace ``x*x+2*x+2`` with ``(Rsqr (x+1))+1``.
Apply ge0_plus_gt0_is_gt0; [Apply pos_Rsqr | Apply Rlt_R0_R1].
Unfold Rsqr; Ring.
Red; Intro; Cut ``0<x*x+1``.
Intro; Rewrite H in H0; Elim (Rlt_antirefl ? H0).
Apply ge0_plus_gt0_is_gt0; [Replace ``x*x`` with (Rsqr x); [Apply pos_Rsqr | Reflexivity] | Apply Rlt_R0_R1].
Qed.
|
