Require Import Reals.
Open Local Scope R_scope.

(* TP7 exercice 1 *)
Lemma Rplus_eq_compat_l: forall r r1 r2, r+r1 = r+r2 -> r1=r2.
intros.
rewrite <- (Rplus_0_l r1).
rewrite <- (Rplus_opp_r r).
rewrite Rplus_comm.
rewrite <- Rplus_assoc.
rewrite (Rplus_comm r1 r).
rewrite H.
rewrite Rplus_comm.
rewrite <- Rplus_assoc.
rewrite (Rplus_comm (-r)).
rewrite Rplus_opp_r.
rewrite Rplus_0_l.
reflexivity.
Qed.

Lemma Rmult_0_r: forall r, r*0=0.
intros.
apply Rplus_eq_compat_l with (r*1).
rewrite <- Rmult_plus_distr_l.
rewrite Rplus_comm.
rewrite Rplus_0_l.
rewrite Rplus_comm.
rewrite Rplus_0_l.
reflexivity.
Qed.

Goal 0 / 0 = 0.
unfold Rdiv.
rewrite Rmult_comm.
apply Rmult_0_r.
Qed.

Lemma Rlt_diff: forall r, ~ r < r.
intros r H.
generalize (Rlt_asym r r).
intros H1; apply H1; trivial.
Qed.

Lemma Rlt_not_eq: forall r1 r2, r1 < r2 -> r1 <> r2.
intros r1 r2 H H1.
apply (Rlt_diff r1).
rewrite H1 at 2.
assumption.
Qed.


Goal 0 <> 2.
apply Rlt_not_eq.
apply Rlt_trans with R1.
apply Rlt_0_1.
rewrite <- (Rplus_0_l 1) at 1.
rewrite Rplus_comm.
apply Rplus_lt_compat_l.
apply Rlt_0_1.
Qed.

(* TP7 exercice 2 *)
Goal forall x, x/2+x/2=x.
intros.
field.
Qed.

Goal forall x y, x<>0 -> y <>0 -> x*y/(x*y) = /y * /(/y).
intros.
field; split; trivial.
Qed.

Goal 232-215 < 64 - 22.
apply Rplus_lt_reg_r with (-17).
ring_simplify.
apply Rplus_lt_pos; auto with real.
repeat apply Rmult_lt_0_compat; auto with real.
apply Rplus_lt_pos; auto with real.
Qed.


(* TP7 exercice 3 *)

Lemma limit_Ropp :
  forall (f:R -> R) (D:R -> Prop) (l x0:R),
    limit1_in f D l x0 -> limit1_in (fun x:R => - f x) D (- l) x0.
intros.
unfold limit1_in, limit_in in *.
intros eps H1.
elim (H eps H1).
intros alp (H2,H3).
exists alp; split; trivial.
intros x (Y1,Y2).
apply Rle_lt_trans with (dist R_met (f x) l).
right.
unfold dist;simpl; unfold R_dist.
replace (-f x --l) with (-(f x-l)) by ring.
apply Rabs_Ropp.
apply H3; split; trivial.
Qed.

Lemma limit_plus :
  forall (f g:R -> R) (D:R -> Prop) (l l' x0:R),
    limit1_in f D l x0 ->
    limit1_in g D l' x0 -> limit1_in (fun x:R => f x + g x) D (l + l') x0.
intros.
unfold limit1_in, limit_in in *.
intros eps Heps.
assert (eps/2 > 0).
apply Rmult_lt_0_compat; auto with real.
elim (H (eps/2)); trivial; clear H.
intros alp1 (Y1,Y2).
elim (H0 (eps/2)); trivial; clear H0.
intros alp2 (Z1,Z2).
exists (Rmin alp1 alp2).
split.
apply Rmin_pos; trivial.
intros x (T1,T2).
replace eps with (eps/2+eps/2) by field.
apply Rle_lt_trans with (dist R_met (f x) l + dist R_met (g x) l').
apply R_dist_plus.
apply Rplus_lt_compat.
apply Y2; split;trivial.
apply Rlt_le_trans with (1:=T2).
apply Rmin_l.
apply Z2; split;trivial.
apply Rlt_le_trans with (1:=T2).
apply Rmin_r.
Qed.

Lemma Dmult_const :
  forall (D:R -> Prop) (f df:R -> R) (x0 a:R),
    D_in f df D x0 -> D_in (fun x:R => a * f x) (fun x:R => a * df x) D x0.
intros D f df x0 a.
case (Req_dec a 0).
intros H H1; rewrite H.
unfold D_in, limit1_in, limit_in.
intros; exists 1; split.
apply Rlt_0_1.
intros.
unfold dist; simpl; unfold R_dist.
replace ((0 * f x - 0 * f x0) / (x - x0) - 0 * df x0) with 0 by (unfold Rdiv; ring).
rewrite Rabs_R0.
exact H0.
intros H.
unfold D_in, limit1_in, limit_in.
intros.
assert (0 < Rabs a).
apply Rabs_pos_lt; trivial.
elim (H0 (eps/(Rabs a))).
intros alp (H3,H4); clear H0.
exists alp; split; trivial.
intros x (Hx1,Hx2).
unfold dist; simpl; unfold R_dist.
replace ((a * f x - a * f x0) / (x - x0) - a * df x0) with
  (a*(((f x - f x0) / (x - x0)) - (df x0))) by (unfold Rdiv; ring).
rewrite Rabs_mult.
apply Rmult_lt_reg_l with (/(Rabs a)); auto with real.
rewrite <- Rmult_assoc.
rewrite Rinv_l; auto with real.
rewrite Rmult_1_l.
rewrite Rmult_comm.
fold (Rdiv eps (Rabs a)).
unfold dist in H4; simpl in H4; unfold R_dist in H4.
apply H4; split; trivial.
apply Rmult_lt_0_compat; auto with real.
Qed.


(* TP7 exercice 4 *)

Lemma exist_cos : forall x:R, { l:R | cos_in x l }.
intros.
apply Alembert_C3.
intros n; unfold cos_n.
apply Rmult_integral_contrapositive_currified.
apply pow_nonzero; auto with real.
apply Rinv_neq_0_compat.
apply not_0_INR.
apply fact_neq_0.
unfold Un_cv.
intros eps Heps.
unfold cos_n.
destruct (archimed_cor1 eps Heps) as (N,(H1,H2)).
exists N; intros n Hn.
unfold R_dist.
rewrite Rminus_0_r.
rewrite Rabs_Rabsolu.
replace ((-1) ^ S n / INR (fact (2 * S n)) / ((-1) ^ n / INR (fact (2 * n))))
  with (-(/(INR ((2*n+1)*(2*n+2))))).
rewrite Rabs_Ropp.
rewrite Rabs_right.
apply Rle_lt_trans with (2:=H1).
apply Rle_Rinv; auto with real zarith.
apply lt_0_INR; auto with arith.
replace ((2 * n + 1) * (2 * n + 2))%nat with
  (S (4*n*n+6*n+1)); auto with arith.
ring.
apply le_INR.
apply le_trans with n; trivial.
replace ((2 * n + 1) * (2 * n + 2))%nat with
  (n + (4*n*n+5*n+2))%nat; auto with arith.
ring.
apply Rle_ge; left.
apply Rinv_0_lt_compat.
apply lt_0_INR.
replace ((2 * n + 1) * (2 * n + 2))%nat with
  (S (4*n*n+6*n+1)); auto with arith.
ring.
apply trans_eq with (((-1) ^ S n / ((-1) ^ n)) * 
  (INR (fact (2 * n)) / INR (fact (2 * S n)))).
pattern (S n) at 1; replace (S n) with (1+n)%nat by omega.
unfold Rdiv; rewrite <- (pow_RN_plus (-1) 1 n); auto with real.
simpl ((-1) ^ 1).
replace (2*(S n))%nat with (S (S (2*n))) by omega.
repeat rewrite fact_simpl.
replace (S (2 * n)) with (2*n+1)%nat by omega.
replace (S (2 * n+1)) with (2*n+2)%nat by omega.
repeat rewrite mult_INR.
field.
split.
apply INR_fact_neq_0.
split; apply not_0_INR.
replace (2*n+1)%nat with (S (2*n)); auto with zarith.
replace (2*n+2)%nat with (S (2*n+1)); auto with zarith.
field.
split.
apply INR_fact_neq_0.
split.
apply INR_fact_neq_0.
apply pow_nonzero; auto with real.
Qed.

Lemma exist_exp : forall x:R, { l:R | exp_in x l }.
intros.
apply Alembert_C3.
intros n.
apply Rinv_neq_0_compat.
apply INR_fact_neq_0.
unfold Un_cv.
intros eps Heps.
destruct (archimed_cor1 eps Heps) as (N,(H1,H2)).
exists N.
intros.
unfold R_dist.
rewrite Rminus_0_r.
rewrite Rabs_Rabsolu.
replace (/ INR (fact (S n)) / / INR (fact n)) with (/(INR (S n))).
rewrite Rabs_right.
apply Rle_lt_trans with (2:=H1).
apply Rle_Rinv; auto with real zarith.
assert (0 < INR (S n)); auto with real.
apply lt_0_INR; auto with arith.
left; apply Rinv_0_lt_compat; auto with real.
rewrite fact_simpl.
rewrite mult_INR.
field.
split.
apply INR_fact_neq_0.
apply not_0_INR; auto.
Qed.