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

forall (f1 f2:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>) (x l1 l2:<a href="Coq.Reals.Rdefinitions.html#R">R</a>),

<a href="Coq.Reals.Ranalysis1.html#derivable_pt_lim">derivable_pt_lim</a> f1 x l1 ->

<a href="Coq.Reals.Ranalysis1.html#derivable_pt_lim">derivable_pt_lim</a> f2 x l2 ->

f2 x <> 0 ->

<a href="Coq.Reals.Ranalysis1.html#derivable_pt_lim">derivable_pt_lim</a> (f1 / f2) x ((l1 * f2 x - l2 * f1 x) / <a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x)).

intros.

cut (<a href="Coq.Reals.Ranalysis1.html#derivable_pt">derivable_pt</a> f2 x);

[ intro | unfold derivable_pt in |- *; apply existT with l2; exact H0 ].

assert (H2:= <a href="Coq.Reals.Ranalysis2.html#continuous_neq_0">continuous_neq_0</a> _ _ (<a href="Coq.Reals.Ranalysis1.html#derivable_continuous_pt">derivable_continuous_pt</a> _ _ X) H1).

elim H2; clear H2; intros eps_f2 H2.

unfold div_fct in |- *.

assert (H3:= <a href="Coq.Reals.Ranalysis1.html#derivable_continuous_pt">derivable_continuous_pt</a> _ _ X).

unfold continuity_pt in H3; unfold continue_in in H3; unfold limit1_in in H3;

unfold limit_in in H3; unfold dist in H3.

simpl in H3; unfold R_dist in H3.

elim (H3 (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 x) / 2));

[ idtac

| unfold Rdiv in |- *; change (0 < <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 x) * / 2) in |- *;

apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>;

[ apply Rabs_pos_lt; assumption | apply Rinv_0_lt_compat; prove_sup0 ] ].

clear H3; intros alp_f2 H3.

cut

(forall x0:<a href="Coq.Reals.Rdefinitions.html#R">R</a>,

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (x0 - x) < alp_f2 -> <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 x0 - f2 x) < <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 x) / 2).

intro H4.

cut (forall a:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (a - x) < alp_f2 -> <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 x) / 2 < <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 a)).

intro H5.

cut

(forall a:<a href="Coq.Reals.Rdefinitions.html#R">R</a>,

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> a < <a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> eps_f2 alp_f2 -> / <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 (x + a)) < 2 / <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 x)).

intro Maj.

unfold derivable_pt_lim in |- *; intros.

elim (H (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (eps * f2 x / 8)));

[ idtac

| unfold Rdiv in |- *; change (0 < <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (eps * f2 x * / 8)) in |- *;

apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_pos_lt">Rabs_pos_lt</a>; repeat apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>;

    [ red in |- *; intro H7; rewrite H7 in H6; elim (Rlt_irrefl _ H6)

| assumption

| apply Rinv_neq_0_compat; discrR ] ].

intros alp_f1d H7.

case (<a href="Coq.Reals.RIneq.html#Req_dec">Req_dec</a> (f1 x) 0); intro.

case (<a href="Coq.Reals.RIneq.html#Req_dec">Req_dec</a> l1 0); intro.

cut (0 < <a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> eps_f2 (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> alp_f2 alp_f1d));

[ intro

| repeat apply <a href="Coq.Reals.Ranalysis2.html#Rmin_pos">Rmin_pos</a>;

    [ apply (cond_pos eps_f2)

| elim H3; intros; assumption

| apply (cond_pos alp_f1d) ] ].

exists (<a href="Coq.Reals.RIneq.html#mkposreal">mkposreal</a> (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> eps_f2 (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> alp_f2 alp_f1d)) H10).

simpl in |- *; intros.

assert (H13:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H12 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

assert (H14:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H12 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

assert (H15:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H13 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

assert (H16:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H13 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

assert (H17:= H7 _ H11 H15).

rewrite <a href="Coq.Reals.Ranalysis2.html#formule">formule</a>; [ idtac | assumption | assumption | apply H2; apply H14 ].

apply <a href="Coq.Reals.RIneq.html#Rle_lt_trans">Rle_lt_trans</a> with

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (/ f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1)) +

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) +

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) +

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (l2 * f1 x / (<a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x))).

unfold Rminus in |- *.

rewrite <-

(<a href="Coq.Reals.Rbasic_fun.html#Rabs_Ropp">Rabs_Ropp</a> (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) + - f2 x) / h + - l2)))

.

apply <a href="Coq.Reals.Ranalysis2.html#Rabs_4">Rabs_4</a>.

repeat rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

apply <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> with (eps / 4 + eps / 4 + eps / 4 + eps / 4).

cut (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (/ f2 (x + h)) * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> ((f1 (x + h) - f1 x) / h - l1) < eps / 4).

cut (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (l1 / (f2 x * f2 (x + h))) * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 x - f2 (x + h)) < eps / 4).

cut

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f1 x / (f2 x * f2 (x + h))) * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> ((f2 (x + h) - f2 x) / h - l2) <

eps / 4).

cut

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (l2 * f1 x / (<a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) * f2 (x + h))) * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 (x + h) - f2 x) <

eps / 4).

intros.

apply <a href="Coq.Reals.Ranalysis2.html#Rlt_4">Rlt_4</a>; assumption.

rewrite H8.

unfold Rdiv in |- *; repeat rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_r">Rmult_0_r</a> || rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>.

rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_R0">Rabs_R0</a>; rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>.

apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>; [ assumption | apply Rinv_0_lt_compat; prove_sup ].

100

rewrite H8.

101

unfold Rdiv in |- *; repeat rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_r">Rmult_0_r</a> || rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>.

102

rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_R0">Rabs_R0</a>; rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>.

103

apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>; [ assumption | apply Rinv_0_lt_compat; prove_sup ].

104

rewrite H9.

105

unfold Rdiv in |- *; repeat rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_r">Rmult_0_r</a> || rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>.

106

rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_R0">Rabs_R0</a>; rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>.

107

apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>; [ assumption | apply Rinv_0_lt_compat; prove_sup ].

108

rewrite <- <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

109

apply (<a href="Coq.Reals.Ranalysis2.html#maj_term1">maj_term1</a> x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2);

110

try assumption || apply H2.

111

apply H14.

112

apply <a href="Coq.Reals.Ranalysis2.html#Rmin_2">Rmin_2</a>; assumption.

113

right; symmetry in |- *; apply <a href="Coq.Reals.Ranalysis2.html#quadruple_var">quadruple_var</a>.

114

assert (H10:= <a href="Coq.Reals.Ranalysis1.html#derivable_continuous_pt">derivable_continuous_pt</a> _ _ X).

115

unfold continuity_pt in H10.

116

unfold continue_in in H10.

117

unfold limit1_in in H10.

118

unfold limit_in in H10.

119

unfold dist in H10.

120

simpl in H10.

121

unfold R_dist in H10.

122

elim (H10 (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (eps * <a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) / (8 * l1)))).

123

clear H10; intros alp_f2t2 H10.

124

cut

125

(forall a:<a href="Coq.Reals.Rdefinitions.html#R">R</a>,

126

127

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 (x + a) - f2 x) < <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (eps * <a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) / (8 * l1))).

128

intro H11.

129

cut (0 < <a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> eps_f2 alp_f1d) (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> alp_f2 alp_f2t2)).

130

intro.

131

exists (<a href="Coq.Reals.RIneq.html#mkposreal">mkposreal</a> (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> eps_f2 alp_f1d) (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> alp_f2 alp_f2t2)) H12).

132

simpl in |- *.

133

intros.

134

assert (H15:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H14 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

135

assert (H16:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H14 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

136

assert (H17:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H15 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

137

assert (H18:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H15 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

138

assert (H19:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H16 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

139

assert (H20:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H16 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

140

clear H14 H15 H16.

141

rewrite <a href="Coq.Reals.Ranalysis2.html#formule">formule</a>; try assumption.

142

apply <a href="Coq.Reals.RIneq.html#Rle_lt_trans">Rle_lt_trans</a> with

143

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (/ f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1)) +

144

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) +

145

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) +

146

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (l2 * f1 x / (<a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x))).

147

unfold Rminus in |- *.

148

rewrite <-

149

(<a href="Coq.Reals.Rbasic_fun.html#Rabs_Ropp">Rabs_Ropp</a> (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) + - f2 x) / h + - l2)))

150

.

151

apply <a href="Coq.Reals.Ranalysis2.html#Rabs_4">Rabs_4</a>.

152

repeat rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

153

apply <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> with (eps / 4 + eps / 4 + eps / 4 + eps / 4).

154

cut (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (/ f2 (x + h)) * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> ((f1 (x + h) - f1 x) / h - l1) < eps / 4).

155

cut (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (l1 / (f2 x * f2 (x + h))) * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 x - f2 (x + h)) < eps / 4).

156

cut

157

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f1 x / (f2 x * f2 (x + h))) * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> ((f2 (x + h) - f2 x) / h - l2) <

158

eps / 4).

159

cut

160

161

eps / 4).

162

intros.

163

apply <a href="Coq.Reals.Ranalysis2.html#Rlt_4">Rlt_4</a>; assumption.

164

rewrite H8.

165

unfold Rdiv in |- *; repeat rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_r">Rmult_0_r</a> || rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>.

166

rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_R0">Rabs_R0</a>; rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>.

167

apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>; [ assumption | apply Rinv_0_lt_compat; prove_sup ].

168

rewrite H8.

169

unfold Rdiv in |- *; repeat rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_r">Rmult_0_r</a> || rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>.

170

rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_R0">Rabs_R0</a>; rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>.

171

apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>; [ assumption | apply Rinv_0_lt_compat; prove_sup ].

172

rewrite <- <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

173

apply (<a href="Coq.Reals.Ranalysis2.html#maj_term2">maj_term2</a> x h eps l1 alp_f2 alp_f2t2 eps_f2 f2); try assumption.

174

apply H2; assumption.

175

apply <a href="Coq.Reals.Ranalysis2.html#Rmin_2">Rmin_2</a>; assumption.

176

rewrite <- <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

177

apply (<a href="Coq.Reals.Ranalysis2.html#maj_term1">maj_term1</a> x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); try assumption.

178

apply H2; assumption.

179

apply <a href="Coq.Reals.Ranalysis2.html#Rmin_2">Rmin_2</a>; assumption.

180

right; symmetry in |- *; apply <a href="Coq.Reals.Ranalysis2.html#quadruple_var">quadruple_var</a>.

181

apply H2; assumption.

182

repeat apply <a href="Coq.Reals.Ranalysis2.html#Rmin_pos">Rmin_pos</a>.

183

apply (<a href="Coq.Reals.RIneq.html#cond_pos">cond_pos</a> eps_f2).

184

apply (<a href="Coq.Reals.RIneq.html#cond_pos">cond_pos</a> alp_f1d).

185

elim H3; intros; assumption.

186

elim H10; intros; assumption.

187

intros.

188

elim H10; intros.

189

case (<a href="Coq.Reals.RIneq.html#Req_dec">Req_dec</a> a 0); intro.

190

rewrite H14; rewrite <a href="Coq.Reals.RIneq.html#Rplus_0_r">Rplus_0_r</a>.

191

unfold Rminus in |- *; rewrite <a href="Coq.Reals.Raxioms.html#Rplus_opp_r">Rplus_opp_r</a>.

192

rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_R0">Rabs_R0</a>.

193

apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_pos_lt">Rabs_pos_lt</a>.

194

unfold Rdiv, Rsqr in |- *; repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>.

195

repeat apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>; try assumption.

196

red in |- *; intro; rewrite H15 in H6; elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H6).

197

apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; repeat apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>; discrR || assumption.

198

apply H13.

199

split.

200

apply <a href="Coq.Reals.Ranalysis2.html#D_x_no_cond">D_x_no_cond</a>; assumption.

201

replace (x + a - x) with a; [ assumption | ring ].

202

change (0 < <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (eps * <a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) / (8 * l1))) in |- *.

203

apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_pos_lt">Rabs_pos_lt</a>; unfold Rdiv, Rsqr in |- *; repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>;

204

repeat apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>.

205

red in |- *; intro; rewrite H11 in H6; elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H6).

206

assumption.

207

assumption.

208

apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; repeat apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>;

209

[ discrR | discrR | discrR | assumption ].

210

case (<a href="Coq.Reals.RIneq.html#Req_dec">Req_dec</a> l1 0); intro.

211

case (<a href="Coq.Reals.RIneq.html#Req_dec">Req_dec</a> l2 0); intro.

212

elim (H0 (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (<a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) * eps / (8 * f1 x))));

213

[ idtac

214

| apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_pos_lt">Rabs_pos_lt</a>; unfold Rdiv, Rsqr in |- *; repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>;

215

repeat apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>;

216

    [ assumption

217

| assumption

218

| red in |- *; intro; rewrite H11 in H6; elim (Rlt_irrefl _ H6)

219

| apply Rinv_neq_0_compat; repeat apply prod_neq_R0; discrR || assumption ] ].

220

intros alp_f2d H12.

221

cut (0 < <a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> eps_f2 alp_f2) (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> alp_f1d alp_f2d)).

222

intro.

223

exists (<a href="Coq.Reals.RIneq.html#mkposreal">mkposreal</a> (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> eps_f2 alp_f2) (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> alp_f1d alp_f2d)) H11).

224

simpl in |- *.

225

intros.

226

assert (H15:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H14 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

227

assert (H16:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H14 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

228

assert (H17:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H15 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

229

assert (H18:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H15 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

230

assert (H19:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H16 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

231

assert (H20:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H16 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

232

clear H15 H16.

233

rewrite <a href="Coq.Reals.Ranalysis2.html#formule">formule</a>; try assumption.

234

apply <a href="Coq.Reals.RIneq.html#Rle_lt_trans">Rle_lt_trans</a> with

235

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (/ f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1)) +

236

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) +

237

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) +

238

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (l2 * f1 x / (<a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x))).

239

unfold Rminus in |- *.

240

rewrite <-

241

(<a href="Coq.Reals.Rbasic_fun.html#Rabs_Ropp">Rabs_Ropp</a> (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) + - f2 x) / h + - l2)))

242

.

243

apply <a href="Coq.Reals.Ranalysis2.html#Rabs_4">Rabs_4</a>.

244

repeat rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

245

apply <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> with (eps / 4 + eps / 4 + eps / 4 + eps / 4).

246

cut (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (/ f2 (x + h)) * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> ((f1 (x + h) - f1 x) / h - l1) < eps / 4).

247

cut (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (l1 / (f2 x * f2 (x + h))) * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 x - f2 (x + h)) < eps / 4).

248

cut

249

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f1 x / (f2 x * f2 (x + h))) * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> ((f2 (x + h) - f2 x) / h - l2) <

250

eps / 4).

251

cut

252

253

eps / 4).

254

intros.

255

apply <a href="Coq.Reals.Ranalysis2.html#Rlt_4">Rlt_4</a>; assumption.

256

rewrite H10.

257

unfold Rdiv in |- *; repeat rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_r">Rmult_0_r</a> || rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>.

258

rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_R0">Rabs_R0</a>; rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>.

259

apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>; [ assumption | apply Rinv_0_lt_compat; prove_sup ].

260

rewrite <- <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

261

apply (<a href="Coq.Reals.Ranalysis2.html#maj_term3">maj_term3</a> x h eps l2 alp_f2 eps_f2 alp_f2d f1 f2); try assumption.

262

apply H2; assumption.

263

apply <a href="Coq.Reals.Ranalysis2.html#Rmin_2">Rmin_2</a>; assumption.

264

rewrite H9.

265

unfold Rdiv in |- *; repeat rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_r">Rmult_0_r</a> || rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>.

266

rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_R0">Rabs_R0</a>; rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>.

267

apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>; [ assumption | apply Rinv_0_lt_compat; prove_sup ].

268

rewrite <- <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

269

apply (<a href="Coq.Reals.Ranalysis2.html#maj_term1">maj_term1</a> x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); assumption || idtac.

270

apply H2; assumption.

271

apply <a href="Coq.Reals.Ranalysis2.html#Rmin_2">Rmin_2</a>; assumption.

272

right; symmetry in |- *; apply <a href="Coq.Reals.Ranalysis2.html#quadruple_var">quadruple_var</a>.

273

apply H2; assumption.

274

repeat apply <a href="Coq.Reals.Ranalysis2.html#Rmin_pos">Rmin_pos</a>.

275

apply (<a href="Coq.Reals.RIneq.html#cond_pos">cond_pos</a> eps_f2).

276

elim H3; intros; assumption.

277

apply (<a href="Coq.Reals.RIneq.html#cond_pos">cond_pos</a> alp_f1d).

278

apply (<a href="Coq.Reals.RIneq.html#cond_pos">cond_pos</a> alp_f2d).

279

elim (H0 (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (<a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) * eps / (8 * f1 x))));

280

 [ idtac

281

| apply Rabs_pos_lt; unfold Rsqr, Rdiv in |- *;

282

repeat rewrite Rinv_mult_distr; repeat apply prod_neq_R0;

283

try assumption || discrR ].

284

intros alp_f2d H11.

285

assert (H12:= <a href="Coq.Reals.Ranalysis1.html#derivable_continuous_pt">derivable_continuous_pt</a> _ _ X).

286

unfold continuity_pt in H12.

287

unfold continue_in in H12.

288

unfold limit1_in in H12.

289

unfold limit_in in H12.

290

unfold dist in H12.

291

simpl in H12.

292

unfold R_dist in H12.

293

elim (H12 (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (<a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) * f2 x * eps / (8 * f1 x * l2)))).

294

intros alp_f2c H13.

295

cut (0 < <a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> eps_f2 alp_f2) (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> alp_f1d (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> alp_f2d alp_f2c))).

296

intro.

297

exists

298

(<a href="Coq.Reals.RIneq.html#mkposreal">mkposreal</a> (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> eps_f2 alp_f2) (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> alp_f1d (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> alp_f2d alp_f2c)))

299

H14).

300

simpl in |- *; intros.

301

assert (H17:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H16 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

302

assert (H18:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H16 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

303

assert (H19:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H18 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

304

assert (H20:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H19 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

305

assert (H21:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H19 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

306

assert (H22:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H18 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

307

assert (H23:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H17 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

308

assert (H24:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H17 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

309

clear H16 H17 H18 H19.

310

cut

311

(forall a:<a href="Coq.Reals.Rdefinitions.html#R">R</a>,

312

313

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 (x + a) - f2 x) <

314

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (<a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) * f2 x * eps / (8 * f1 x * l2))).

315

intro.

316

rewrite <a href="Coq.Reals.Ranalysis2.html#formule">formule</a>; try assumption.

317

apply <a href="Coq.Reals.RIneq.html#Rle_lt_trans">Rle_lt_trans</a> with

318

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (/ f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1)) +

319

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) +

320

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) +

321

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (l2 * f1 x / (<a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x))).

322

unfold Rminus in |- *.

323

rewrite <-

324

(<a href="Coq.Reals.Rbasic_fun.html#Rabs_Ropp">Rabs_Ropp</a> (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) + - f2 x) / h + - l2)))

325

.

326

apply <a href="Coq.Reals.Ranalysis2.html#Rabs_4">Rabs_4</a>.

327

repeat rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

328

apply <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> with (eps / 4 + eps / 4 + eps / 4 + eps / 4).

329

cut (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (/ f2 (x + h)) * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> ((f1 (x + h) - f1 x) / h - l1) < eps / 4).

330

cut (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (l1 / (f2 x * f2 (x + h))) * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 x - f2 (x + h)) < eps / 4).

331

cut

332

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f1 x / (f2 x * f2 (x + h))) * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> ((f2 (x + h) - f2 x) / h - l2) <

333

eps / 4).

334

cut

335

336

eps / 4).

337

intros.

338

apply <a href="Coq.Reals.Ranalysis2.html#Rlt_4">Rlt_4</a>; assumption.

339

rewrite <- <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

340

apply (<a href="Coq.Reals.Ranalysis2.html#maj_term4">maj_term4</a> x h eps l2 alp_f2 alp_f2c eps_f2 f1 f2); try assumption.

341

apply H2; assumption.

342

apply <a href="Coq.Reals.Ranalysis2.html#Rmin_2">Rmin_2</a>; assumption.

343

rewrite <- <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

344

apply (<a href="Coq.Reals.Ranalysis2.html#maj_term3">maj_term3</a> x h eps l2 alp_f2 eps_f2 alp_f2d f1 f2); try assumption.

345

apply H2; assumption.

346

apply <a href="Coq.Reals.Ranalysis2.html#Rmin_2">Rmin_2</a>; assumption.

347

rewrite H9.

348

unfold Rdiv in |- *; repeat rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_r">Rmult_0_r</a> || rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>.

349

rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_R0">Rabs_R0</a>; rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>.

350

apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>; [ assumption | apply Rinv_0_lt_compat; prove_sup ].

351

rewrite <- <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

352

apply (<a href="Coq.Reals.Ranalysis2.html#maj_term1">maj_term1</a> x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); try assumption.

353

apply H2; assumption.

354

apply <a href="Coq.Reals.Ranalysis2.html#Rmin_2">Rmin_2</a>; assumption.

355

right; symmetry in |- *; apply <a href="Coq.Reals.Ranalysis2.html#quadruple_var">quadruple_var</a>.

356

apply H2; assumption.

357

intros.

358

case (<a href="Coq.Reals.RIneq.html#Req_dec">Req_dec</a> a 0); intro.

359

rewrite H17; rewrite <a href="Coq.Reals.RIneq.html#Rplus_0_r">Rplus_0_r</a>.

360

unfold Rminus in |- *; rewrite <a href="Coq.Reals.Raxioms.html#Rplus_opp_r">Rplus_opp_r</a>; rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_R0">Rabs_R0</a>.

361

apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_pos_lt">Rabs_pos_lt</a>.

362

unfold Rdiv, Rsqr in |- *.

363

repeat rewrite <a href="Coq.Reals.RIneq.html#Rinv_mult_distr">Rinv_mult_distr</a>; try assumption.

364

repeat apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>; try assumption.

365

red in |- *; intro H18; rewrite H18 in H6; elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H6).

366

apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; discrR.

367

apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; discrR.

368

apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; discrR.

369

apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; assumption.

370

apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; assumption.

371

discrR.

372

discrR.

373

discrR.

374

discrR.

375

discrR.

376

apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>; [ discrR | assumption ].

377

elim H13; intros.

378

apply H19.

379

split.

380

apply <a href="Coq.Reals.Ranalysis2.html#D_x_no_cond">D_x_no_cond</a>; assumption.

381

replace (x + a - x) with a; [ assumption | ring ].

382

repeat apply <a href="Coq.Reals.Ranalysis2.html#Rmin_pos">Rmin_pos</a>.

383

apply (<a href="Coq.Reals.RIneq.html#cond_pos">cond_pos</a> eps_f2).

384

elim H3; intros; assumption.

385

apply (<a href="Coq.Reals.RIneq.html#cond_pos">cond_pos</a> alp_f1d).

386

apply (<a href="Coq.Reals.RIneq.html#cond_pos">cond_pos</a> alp_f2d).

387

elim H13; intros; assumption.

388

change (0 < <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (<a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) * f2 x * eps / (8 * f1 x * l2))) in |- *.

389

apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_pos_lt">Rabs_pos_lt</a>.

390

unfold Rsqr, Rdiv in |- *.

391

repeat rewrite <a href="Coq.Reals.RIneq.html#Rinv_mult_distr">Rinv_mult_distr</a>; try assumption || discrR.

392

repeat apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>; try assumption.

393

red in |- *; intro H13; rewrite H13 in H6; elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H6).

394

apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; discrR.

395

apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; discrR.

396

apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; discrR.

397

apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; assumption.

398

apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; assumption.

399

apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>; [ discrR | assumption ].

400

red in |- *; intro H11; rewrite H11 in H6; elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H6).

401

apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; discrR.

402

apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; discrR.

403

apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; discrR.

404

apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; assumption.

405

case (<a href="Coq.Reals.RIneq.html#Req_dec">Req_dec</a> l2 0); intro.

406

assert (H11:= <a href="Coq.Reals.Ranalysis1.html#derivable_continuous_pt">derivable_continuous_pt</a> _ _ X).

407

unfold continuity_pt in H11.

408

unfold continue_in in H11.

409

unfold limit1_in in H11.

410

unfold limit_in in H11.

411

unfold dist in H11.

412

simpl in H11.

413

unfold R_dist in H11.

414

elim (H11 (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (eps * <a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) / (8 * l1)))).

415

clear H11; intros alp_f2t2 H11.

416

elim (H0 (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (<a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) * eps / (8 * f1 x)))).

417

intros alp_f2d H12.

418

419

intro.

420

exists

421

(<a href="Coq.Reals.RIneq.html#mkposreal">mkposreal</a>

422

(<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> eps_f2 alp_f2) (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> alp_f1d (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> alp_f2d alp_f2t2))) H13).

423

simpl in |- *.

424

intros.

425

cut

426

(forall a:<a href="Coq.Reals.Rdefinitions.html#R">R</a>,

427

428

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 (x + a) - f2 x) < <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (eps * <a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) / (8 * l1))).

429

intro.

430

assert (H17:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H15 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

431

assert (H18:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H15 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

432

assert (H19:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H17 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

433

assert (H20:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H17 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

434

assert (H21:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H18 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

435

assert (H22:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H18 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

436

assert (H23:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H21 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

437

assert (H24:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H21 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

438

clear H15 H17 H18 H21.

439

rewrite <a href="Coq.Reals.Ranalysis2.html#formule">formule</a>; try assumption.

440

apply <a href="Coq.Reals.RIneq.html#Rle_lt_trans">Rle_lt_trans</a> with

441

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (/ f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1)) +

442

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) +

443

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) +

444

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (l2 * f1 x / (<a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x))).

445

unfold Rminus in |- *.

446

rewrite <-

447

(<a href="Coq.Reals.Rbasic_fun.html#Rabs_Ropp">Rabs_Ropp</a> (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) + - f2 x) / h + - l2)))

448

.

449

apply <a href="Coq.Reals.Ranalysis2.html#Rabs_4">Rabs_4</a>.

450

repeat rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

451

apply <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> with (eps / 4 + eps / 4 + eps / 4 + eps / 4).

452

cut (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (/ f2 (x + h)) * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> ((f1 (x + h) - f1 x) / h - l1) < eps / 4).

453

cut (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (l1 / (f2 x * f2 (x + h))) * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 x - f2 (x + h)) < eps / 4).

454

cut

455

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f1 x / (f2 x * f2 (x + h))) * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> ((f2 (x + h) - f2 x) / h - l2) <

456

eps / 4).

457

cut

458

459

eps / 4).

460

intros.

461

apply <a href="Coq.Reals.Ranalysis2.html#Rlt_4">Rlt_4</a>; assumption.

462

rewrite H10.

463

unfold Rdiv in |- *; repeat rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_r">Rmult_0_r</a> || rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>.

464

rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_R0">Rabs_R0</a>; rewrite <a href="Coq.Reals.RIneq.html#Rmult_0_l">Rmult_0_l</a>.

465

apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>; [ assumption | apply Rinv_0_lt_compat; prove_sup ].

466

rewrite <- <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

467

apply (<a href="Coq.Reals.Ranalysis2.html#maj_term3">maj_term3</a> x h eps l2 alp_f2 eps_f2 alp_f2d f1 f2); try assumption.

468

apply H2; assumption.

469

apply <a href="Coq.Reals.Ranalysis2.html#Rmin_2">Rmin_2</a>; assumption.

470

rewrite <- <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

471

apply (<a href="Coq.Reals.Ranalysis2.html#maj_term2">maj_term2</a> x h eps l1 alp_f2 alp_f2t2 eps_f2 f2); try assumption.

472

apply H2; assumption.

473

apply <a href="Coq.Reals.Ranalysis2.html#Rmin_2">Rmin_2</a>; assumption.

474

rewrite <- <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

475

apply (<a href="Coq.Reals.Ranalysis2.html#maj_term1">maj_term1</a> x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); try assumption.

476

apply H2; assumption.

477

apply <a href="Coq.Reals.Ranalysis2.html#Rmin_2">Rmin_2</a>; assumption.

478

right; symmetry in |- *; apply <a href="Coq.Reals.Ranalysis2.html#quadruple_var">quadruple_var</a>.

479

apply H2; assumption.

480

intros.

481

case (<a href="Coq.Reals.RIneq.html#Req_dec">Req_dec</a> a 0); intro.

482

rewrite H17; rewrite <a href="Coq.Reals.RIneq.html#Rplus_0_r">Rplus_0_r</a>; unfold Rminus in |- *; rewrite <a href="Coq.Reals.Raxioms.html#Rplus_opp_r">Rplus_opp_r</a>;

483

rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_R0">Rabs_R0</a>.

484

apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_pos_lt">Rabs_pos_lt</a>.

485

unfold Rdiv in |- *; rewrite <a href="Coq.Reals.RIneq.html#Rinv_mult_distr">Rinv_mult_distr</a>; try discrR || assumption.

486

unfold Rsqr in |- *.

487

repeat apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>;

488

assumption ||

489

(apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; assumption) ||

490

(apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; discrR) ||

491

(red in |- *; intro H18; rewrite H18 in H6; elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H6)).

492

elim H11; intros.

493

apply H19.

494

split.

495

apply <a href="Coq.Reals.Ranalysis2.html#D_x_no_cond">D_x_no_cond</a>; assumption.

496

replace (x + a - x) with a; [ assumption | ring ].

497

repeat apply <a href="Coq.Reals.Ranalysis2.html#Rmin_pos">Rmin_pos</a>.

498

apply (<a href="Coq.Reals.RIneq.html#cond_pos">cond_pos</a> eps_f2).

499

elim H3; intros; assumption.

500

apply (<a href="Coq.Reals.RIneq.html#cond_pos">cond_pos</a> alp_f1d).

501

apply (<a href="Coq.Reals.RIneq.html#cond_pos">cond_pos</a> alp_f2d).

502

elim H11; intros; assumption.

503

apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_pos_lt">Rabs_pos_lt</a>.

504

unfold Rdiv, Rsqr in |- *; rewrite <a href="Coq.Reals.RIneq.html#Rinv_mult_distr">Rinv_mult_distr</a>; try discrR || assumption.

505

repeat apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>;

506

assumption ||

507

(apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; assumption) ||

508

(apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; discrR) ||

509

(red in |- *; intro H12; rewrite H12 in H6; elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H6)).

510

change (0 < <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (eps * <a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) / (8 * l1))) in |- *.

511

apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_pos_lt">Rabs_pos_lt</a>.

512

unfold Rdiv, Rsqr in |- *; rewrite <a href="Coq.Reals.RIneq.html#Rinv_mult_distr">Rinv_mult_distr</a>; try discrR || assumption.

513

repeat apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>;

514

assumption ||

515

(apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; assumption) ||

516

(apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; discrR) ||

517

(red in |- *; intro H12; rewrite H12 in H6; elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H6)).

518

elim (H0 (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (<a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) * eps / (8 * f1 x)))).

519

intros alp_f2d H11.

520

assert (H12:= <a href="Coq.Reals.Ranalysis1.html#derivable_continuous_pt">derivable_continuous_pt</a> _ _ X).

521

unfold continuity_pt in H12.

522

unfold continue_in in H12.

523

unfold limit1_in in H12.

524

unfold limit_in in H12.

525

unfold dist in H12.

526

simpl in H12.

527

unfold R_dist in H12.

528

elim (H12 (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (<a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) * f2 x * eps / (8 * f1 x * l2)))).

529

intros alp_f2c H13.

530

elim (H12 (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (eps * <a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) / (8 * l1)))).

531

intros alp_f2t2 H14.

532

cut

533

(0 <

534

<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> eps_f2 alp_f2) (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> alp_f1d alp_f2d))

535

(<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> alp_f2c alp_f2t2)).

536

intro.

537

exists

538

(<a href="Coq.Reals.RIneq.html#mkposreal">mkposreal</a>

539

(<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> eps_f2 alp_f2) (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> alp_f1d alp_f2d))

540

(<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> alp_f2c alp_f2t2)) H15).

541

simpl in |- *.

542

intros.

543

assert (H18:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H17 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

544

assert (H19:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H17 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

545

assert (H20:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H18 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

546

assert (H21:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H18 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

547

assert (H22:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H19 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

548

assert (H23:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H19 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

549

assert (H24:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H20 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

550

assert (H25:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H20 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

551

assert (H26:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H21 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)).

552

assert (H27:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H21 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)).

553

clear H17 H18 H19 H20 H21.

554

cut

555

(forall a:<a href="Coq.Reals.Rdefinitions.html#R">R</a>,

556

557

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 (x + a) - f2 x) < <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (eps * <a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) / (8 * l1))).

558

cut

559

(forall a:<a href="Coq.Reals.Rdefinitions.html#R">R</a>,

560

561

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 (x + a) - f2 x) <

562

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (<a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) * f2 x * eps / (8 * f1 x * l2))).

563

intros.

564

rewrite <a href="Coq.Reals.Ranalysis2.html#formule">formule</a>; try assumption.

565

apply <a href="Coq.Reals.RIneq.html#Rle_lt_trans">Rle_lt_trans</a> with

566

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (/ f2 (x + h) * ((f1 (x + h) - f1 x) / h - l1)) +

567

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (l1 / (f2 x * f2 (x + h)) * (f2 x - f2 (x + h))) +

568

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) +

569

<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (l2 * f1 x / (<a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) * f2 (x + h)) * (f2 (x + h) - f2 x))).

570

unfold Rminus in |- *.

571

rewrite <-

572

(<a href="Coq.Reals.Rbasic_fun.html#Rabs_Ropp">Rabs_Ropp</a> (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) + - f2 x) / h + - l2)))

573

.

574

apply <a href="Coq.Reals.Ranalysis2.html#Rabs_4">Rabs_4</a>.

575

repeat rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

576

apply <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> with (eps / 4 + eps / 4 + eps / 4 + eps / 4).

577

cut (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (/ f2 (x + h)) * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> ((f1 (x + h) - f1 x) / h - l1) < eps / 4).

578

cut (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (l1 / (f2 x * f2 (x + h))) * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 x - f2 (x + h)) < eps / 4).

579

cut

580

(<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f1 x / (f2 x * f2 (x + h))) * <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> ((f2 (x + h) - f2 x) / h - l2) <

581

eps / 4).

582

cut

583

584

eps / 4).

585

intros.

586

apply <a href="Coq.Reals.Ranalysis2.html#Rlt_4">Rlt_4</a>; assumption.

587

rewrite <- <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

588

apply (<a href="Coq.Reals.Ranalysis2.html#maj_term4">maj_term4</a> x h eps l2 alp_f2 alp_f2c eps_f2 f1 f2); try assumption.

589

apply H2; assumption.

590

apply <a href="Coq.Reals.Ranalysis2.html#Rmin_2">Rmin_2</a>; assumption.

591

rewrite <- <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

592

apply (<a href="Coq.Reals.Ranalysis2.html#maj_term3">maj_term3</a> x h eps l2 alp_f2 eps_f2 alp_f2d f1 f2); try assumption.

593

apply H2; assumption.

594

apply <a href="Coq.Reals.Ranalysis2.html#Rmin_2">Rmin_2</a>; assumption.

595

rewrite <- <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

596

apply (<a href="Coq.Reals.Ranalysis2.html#maj_term2">maj_term2</a> x h eps l1 alp_f2 alp_f2t2 eps_f2 f2); try assumption.

597

apply H2; assumption.

598

apply <a href="Coq.Reals.Ranalysis2.html#Rmin_2">Rmin_2</a>; assumption.

599

rewrite <- <a href="Coq.Reals.Rbasic_fun.html#Rabs_mult">Rabs_mult</a>.

600

apply (<a href="Coq.Reals.Ranalysis2.html#maj_term1">maj_term1</a> x h eps l1 alp_f2 eps_f2 alp_f1d f1 f2); try assumption.

601

apply H2; assumption.

602

apply <a href="Coq.Reals.Ranalysis2.html#Rmin_2">Rmin_2</a>; assumption.

603

right; symmetry in |- *; apply <a href="Coq.Reals.Ranalysis2.html#quadruple_var">quadruple_var</a>.

604

apply H2; assumption.

605

intros.

606

case (<a href="Coq.Reals.RIneq.html#Req_dec">Req_dec</a> a 0); intro.

607

rewrite H18; rewrite <a href="Coq.Reals.RIneq.html#Rplus_0_r">Rplus_0_r</a>; unfold Rminus in |- *; rewrite <a href="Coq.Reals.Raxioms.html#Rplus_opp_r">Rplus_opp_r</a>;

608

rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_R0">Rabs_R0</a>; apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_pos_lt">Rabs_pos_lt</a>.

609

unfold Rdiv, Rsqr in |- *; rewrite <a href="Coq.Reals.RIneq.html#Rinv_mult_distr">Rinv_mult_distr</a>.

610

repeat apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>;

611

assumption ||

612

(apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; assumption) ||

613

(apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; discrR) ||

614

(red in |- *; intro H28; rewrite H28 in H6; elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H6)).

615

apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>; [ discrR | assumption ].

616

apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>; [ discrR | assumption ].

617

assumption.

618

elim H13; intros.

619

apply H20.

620

split.

621

apply <a href="Coq.Reals.Ranalysis2.html#D_x_no_cond">D_x_no_cond</a>; assumption.

622

replace (x + a - x) with a; [ assumption | ring ].

623

intros.

624

case (<a href="Coq.Reals.RIneq.html#Req_dec">Req_dec</a> a 0); intro.

625

rewrite H18; rewrite <a href="Coq.Reals.RIneq.html#Rplus_0_r">Rplus_0_r</a>; unfold Rminus in |- *; rewrite <a href="Coq.Reals.Raxioms.html#Rplus_opp_r">Rplus_opp_r</a>;

626

rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_R0">Rabs_R0</a>; apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_pos_lt">Rabs_pos_lt</a>.

627

unfold Rdiv, Rsqr in |- *; rewrite <a href="Coq.Reals.RIneq.html#Rinv_mult_distr">Rinv_mult_distr</a>.

628

repeat apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>;

629

assumption ||

630

(apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; assumption) ||

631

(apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; discrR) ||

632

(red in |- *; intro H28; rewrite H28 in H6; elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H6)).

633

discrR.

634

assumption.

635

elim H14; intros.

636

apply H20.

637

split.

638

unfold D_x, no_cond in |- *; split.

639

trivial.

640

apply <a href="Coq.Reals.RIneq.html#Rminus_not_eq_right">Rminus_not_eq_right</a>.

641

replace (x + a - x) with a; [ assumption | ring ].

642

replace (x + a - x) with a; [ assumption | ring ].

643

repeat apply <a href="Coq.Reals.Ranalysis2.html#Rmin_pos">Rmin_pos</a>.

644

apply (<a href="Coq.Reals.RIneq.html#cond_pos">cond_pos</a> eps_f2).

645

elim H3; intros; assumption.

646

apply (<a href="Coq.Reals.RIneq.html#cond_pos">cond_pos</a> alp_f1d).

647

apply (<a href="Coq.Reals.RIneq.html#cond_pos">cond_pos</a> alp_f2d).

648

elim H13; intros; assumption.

649

elim H14; intros; assumption.

650

change (0 < <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (eps * <a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) / (8 * l1))) in |- *; apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_pos_lt">Rabs_pos_lt</a>.

651

unfold Rdiv, Rsqr in |- *; rewrite <a href="Coq.Reals.RIneq.html#Rinv_mult_distr">Rinv_mult_distr</a>; try discrR || assumption.

652

repeat apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>;

653

assumption ||

654

(apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; assumption) ||

655

(apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; discrR) ||

656

(red in |- *; intro H14; rewrite H14 in H6; elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H6)).

657

change (0 < <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (<a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x) * f2 x * eps / (8 * f1 x * l2))) in |- *;

658

apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_pos_lt">Rabs_pos_lt</a>.

659

unfold Rdiv, Rsqr in |- *; rewrite <a href="Coq.Reals.RIneq.html#Rinv_mult_distr">Rinv_mult_distr</a>.

660

repeat apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>;

661

assumption ||

662

(apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; assumption) ||

663

(apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; discrR) ||

664

(red in |- *; intro H13; rewrite H13 in H6; elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H6)).

665

apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>; [ discrR | assumption ].

666

apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>; [ discrR | assumption ].

667

assumption.

668

apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_pos_lt">Rabs_pos_lt</a>.

669

unfold Rdiv, Rsqr in |- *; rewrite <a href="Coq.Reals.RIneq.html#Rinv_mult_distr">Rinv_mult_distr</a>;

670

[ idtac | discrR | assumption ].

671

repeat apply <a href="Coq.Reals.RIneq.html#prod_neq_R0">prod_neq_R0</a>;

672

assumption ||

673

(apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; assumption) ||

674

(apply <a href="Coq.Reals.RIneq.html#Rinv_neq_0_compat">Rinv_neq_0_compat</a>; discrR) ||

675

(red in |- *; intro H11; rewrite H11 in H6; elim (<a href="Coq.Reals.RIneq.html#Rlt_irrefl">Rlt_irrefl</a> _ H6)).

676

intros.

677

unfold Rdiv in |- *.

678

apply <a href="Coq.Reals.RIneq.html#Rmult_lt_reg_l">Rmult_lt_reg_l</a> with (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 (x + a))).

679

apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_pos_lt">Rabs_pos_lt</a>; apply H2.

680

apply <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> with (<a href="Coq.Reals.Rbasic_fun.html#Rmin">Rmin</a> eps_f2 alp_f2).

681

assumption.

682

apply <a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a>.

683

rewrite <- <a href="Coq.Reals.RIneq.html#Rinv_r_sym">Rinv_r_sym</a>.

684

apply <a href="Coq.Reals.RIneq.html#Rmult_lt_reg_l">Rmult_lt_reg_l</a> with (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 x)).

685

apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_pos_lt">Rabs_pos_lt</a>; assumption.

686

rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>.

687

rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (<a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 x))).

688

repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>.

689

rewrite <- <a href="Coq.Reals.RIneq.html#Rinv_l_sym">Rinv_l_sym</a>.

690

rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>.

691

apply <a href="Coq.Reals.RIneq.html#Rmult_lt_reg_l">Rmult_lt_reg_l</a> with (/ 2).

692

apply <a href="Coq.Reals.RIneq.html#Rinv_0_lt_compat">Rinv_0_lt_compat</a>; prove_sup0.

693

repeat rewrite (<a href="Coq.Reals.Raxioms.html#Rmult_comm">Rmult_comm</a> (/ 2)).

694

repeat rewrite <a href="Coq.Reals.Raxioms.html#Rmult_assoc">Rmult_assoc</a>.

695

rewrite <- <a href="Coq.Reals.RIneq.html#Rinv_r_sym">Rinv_r_sym</a>.

696

rewrite <a href="Coq.Reals.RIneq.html#Rmult_1_r">Rmult_1_r</a>.

697

unfold Rdiv in H5; apply H5.

698

replace (x + a - x) with a.

699

assert (H7:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H6 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_r">Rmin_r</a> _ _)); assumption.

700

ring.

701

discrR.

702

apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_no_R0">Rabs_no_R0</a>; assumption.

703

apply <a href="Coq.Reals.Rbasic_fun.html#Rabs_no_R0">Rabs_no_R0</a>; apply H2.

704

assert (H7:= <a href="Coq.Reals.RIneq.html#Rlt_le_trans">Rlt_le_trans</a> _ _ _ H6 (<a href="Coq.Reals.Rbasic_fun.html#Rmin_l">Rmin_l</a> _ _)); assumption.

705

intros.

706

assert (H6:= H4 a H5).

707

rewrite <- (<a href="Coq.Reals.Rbasic_fun.html#Rabs_Ropp">Rabs_Ropp</a> (f2 a - f2 x)) in H6.

708

rewrite <a href="Coq.Reals.RIneq.html#Ropp_minus_distr">Ropp_minus_distr</a> in H6.

709

assert (H7:= <a href="Coq.Reals.RIneq.html#Rle_lt_trans">Rle_lt_trans</a> _ _ _ (<a href="Coq.Reals.Rbasic_fun.html#Rabs_triang_inv">Rabs_triang_inv</a> _ _) H6).

710

apply <a href="Coq.Reals.RIneq.html#Rplus_lt_reg_r">Rplus_lt_reg_r</a> with (- <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 a) + <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 x) / 2).

711

rewrite <a href="Coq.Reals.Raxioms.html#Rplus_assoc">Rplus_assoc</a>.

712

rewrite <- <a href="Coq.Reals.RIneq.html#double_var">double_var</a>.

713

do 2 rewrite (<a href="Coq.Reals.Raxioms.html#Rplus_comm">Rplus_comm</a> (- <a href="Coq.Reals.Rbasic_fun.html#Rabs">Rabs</a> (f2 a))).

714

rewrite <a href="Coq.Reals.Raxioms.html#Rplus_assoc">Rplus_assoc</a>; rewrite <a href="Coq.Reals.RIneq.html#Rplus_opp_l">Rplus_opp_l</a>; rewrite <a href="Coq.Reals.RIneq.html#Rplus_0_r">Rplus_0_r</a>.

715

unfold Rminus in H7; assumption.

716

intros.

717

case (<a href="Coq.Reals.RIneq.html#Req_dec">Req_dec</a> x x0); intro.

718

rewrite <- H5; unfold Rminus in |- *; rewrite <a href="Coq.Reals.Raxioms.html#Rplus_opp_r">Rplus_opp_r</a>; rewrite <a href="Coq.Reals.Rbasic_fun.html#Rabs_R0">Rabs_R0</a>;

719

unfold Rdiv in |- *; apply <a href="Coq.Reals.RIneq.html#Rmult_lt_0_compat">Rmult_lt_0_compat</a>;

720

[ apply Rabs_pos_lt; assumption | apply Rinv_0_lt_compat; prove_sup0 ].

721

elim H3; intros.

722

apply H7.

723

split.

724

unfold D_x, no_cond in |- *; split.

725

trivial.

726

assumption.

727

assumption.

728

<code class="keyword">Qed</code>.

729

730

731

<code class="keyword">Lemma</code> <a name="derivable_pt_div"></a>derivable_pt_div :

732

forall (f1 f2:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>) (x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>),

733

<a href="Coq.Reals.Ranalysis1.html#derivable_pt">derivable_pt</a> f1 x ->

734

<a href="Coq.Reals.Ranalysis1.html#derivable_pt">derivable_pt</a> f2 x -> f2 x <> 0 -> <a href="Coq.Reals.Ranalysis1.html#derivable_pt">derivable_pt</a> (f1 / f2) x.

735

unfold derivable_pt in |- *.

736

intros.

737

elim X; intros.

738

elim X0; intros.

739

apply <a href="Coq.Init.Specif.html#existT">existT</a> with ((x0 * f2 x - x1 * f1 x) / <a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x)).

740

apply <a href="Coq.Reals.Ranalysis3.html#derivable_pt_lim_div">derivable_pt_lim_div</a>; assumption.

741

<code class="keyword">Qed</code>.

742

743

744

<code class="keyword">Lemma</code> <a name="derivable_div"></a>derivable_div :

745

forall f1 f2:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>,

746

<a href="Coq.Reals.Ranalysis1.html#derivable">derivable</a> f1 ->

747

<a href="Coq.Reals.Ranalysis1.html#derivable">derivable</a> f2 -> (forall x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>, f2 x <> 0) -> <a href="Coq.Reals.Ranalysis1.html#derivable">derivable</a> (f1 / f2).

748

unfold derivable in |- *; intros.

749

apply (<a href="Coq.Reals.Ranalysis3.html#derivable_pt_div">derivable_pt_div</a> _ _ _ (X x) (X0 x) (H x)).

750

<code class="keyword">Qed</code>.

751

752

753

<code class="keyword">Lemma</code> <a name="derive_pt_div"></a>derive_pt_div :

754

forall (f1 f2:<a href="Coq.Reals.Rdefinitions.html#R">R</a> -> <a href="Coq.Reals.Rdefinitions.html#R">R</a>) (x:<a href="Coq.Reals.Rdefinitions.html#R">R</a>) (pr1:<a href="Coq.Reals.Ranalysis1.html#derivable_pt">derivable_pt</a> f1 x)

755

(pr2:<a href="Coq.Reals.Ranalysis1.html#derivable_pt">derivable_pt</a> f2 x) (na:f2 x <> 0),

756

<a href="Coq.Reals.Ranalysis1.html#derive_pt">derive_pt</a> (f1 / f2) x (<a href="Coq.Reals.Ranalysis3.html#derivable_pt_div">derivable_pt_div</a> _ _ _ pr1 pr2 na) =

757

(<a href="Coq.Reals.Ranalysis1.html#derive_pt">derive_pt</a> f1 x pr1 * f2 x - <a href="Coq.Reals.Ranalysis1.html#derive_pt">derive_pt</a> f2 x pr2 * f1 x) / <a href="Coq.Reals.RIneq.html#Rsqr">Rsqr</a> (f2 x).

758

intros.

759

assert (H:= <a href="Coq.Reals.Ranalysis1.html#derivable_derive">derivable_derive</a> f1 x pr1).

760

assert (H0:= <a href="Coq.Reals.Ranalysis1.html#derivable_derive">derivable_derive</a> f2 x pr2).

761

assert

762

(H1:= <a href="Coq.Reals.Ranalysis1.html#derivable_derive">derivable_derive</a> (f1 / f2)%F x (<a href="Coq.Reals.Ranalysis3.html#derivable_pt_div">derivable_pt_div</a> _ _ _ pr1 pr2 na)).

763

elim H; clear H; intros l1 H.

764

elim H0; clear H0; intros l2 H0.

765

elim H1; clear H1; intros l H1.

766

rewrite H; rewrite H0; apply <a href="Coq.Reals.Ranalysis1.html#derive_pt_eq_0">derive_pt_eq_0</a>.

767

assert (H3:= <a href="Coq.Init.Specif.html#projT2">projT2</a> pr1).

768

unfold derive_pt in H; rewrite H in H3.

769

assert (H4:= <a href="Coq.Init.Specif.html#projT2">projT2</a> pr2).

770

unfold derive_pt in H0; rewrite H0 in H4.

771

apply <a href="Coq.Reals.Ranalysis3.html#derivable_pt_lim_div">derivable_pt_lim_div</a>; assumption.

772

773

<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://www.lri.fr/~filliatr/coqdoc/">coqdoc</a>

774

</body>

775

</html>

b'\\ No newline at end of file'

Older »