coq_practice_28.v

Require Import Reals.
Require Import Fourier.

Theorem PI_RGT_3_05 : (PI > 3 + 5/100)%R.
Proof.
  assert (((sum_f_R0 (tg_alt PI_tg) (S (2 * 5)))%R <= (PI / 4)%R <=
    (sum_f_R0 (tg_alt PI_tg) (2 * 5))%R)%R).
  apply PI_ineq.
  simpl H.
  destruct H.
  assert (((sum_f_R0 (tg_alt PI_tg) (S(2 * 5)))*4)<=PI).
    assert (PI = PI/4*4).
      field.
    rewrite H1.
    apply Rmult_le_compat_r.
    fourier.
    apply H.
  apply (Rge_gt_trans PI (sum_f_R0 (tg_alt PI_tg) (S (2 * 5)) * 4 ) (3 + 5 / 100)).
    fourier.
  simpl.
  unfold tg_alt.
  unfold PI_tg.
  unfold INR.
  simpl.
  field_simplify.

  apply  Rminus_gt.
  field_simplify.
  assert (0/1 = 0).
  field.
  rewrite H2.
  prove_sup.
  apply Rinv_0_lt_compat.
  prove_sup.
Qed.