C以外

6.v

Module Q26.
Require Import NArith.
Goal (221 * 293 * 389 * 397 + 17 = 14 * 119 * 127 * 151 * 313)%nat.
Proof.
  apply Nat2N.inj.
  rewrite Nat2N.inj_add.
  rewrite Nat2N.inj_mul. rewrite Nat2N.inj_mul. rewrite Nat2N.inj_mul.
  rewrite Nat2N.inj_mul. rewrite Nat2N.inj_mul.
  rewrite Nat2N.inj_mul. rewrite Nat2N.inj_mul.
  simpl. reflexivity.
Qed.
End Q26.

Module Q27.
Require Import ZArith.

Lemma hoge : forall z : Z, (z ^ 4 - 4 * z ^ 2 + 4 > 0)%Z.
Proof.
  intro z.
  replace (z^4 - 4*z^2 + 4)%Z with ((z*z - 2) * (z*z - 2))%Z by ring.
  assert (Hge : ((z*z - 2) * (z*z - 2) >= 0)%Z) by apply sqr_pos.
  assert (Hne : ((z*z - 2) * (z*z - 2) <> 0)%Z).
    intro H1. apply Zmult_integral in H1.
    assert (H2 : (z*z - 2)%Z = 0%Z) by (destruct H1; assumption); clear H1.
    assert (H : (z*z)%Z = 2%Z).
      apply Zeq_plus_swap in H2. rewrite H2. ring.
    clear H2.
    assert (Habs : (Z.abs z * Z.abs z = z * z)%Z) by (destruct z; reflexivity).
    assert (Hup : (Z.abs z < 2)%Z).
      apply Zlt_square_simpl. omega. rewrite Habs. rewrite H. omega.
    assert (Hlo : (1 < Z.abs z)%Z).
      apply Zlt_square_simpl. destruct z; compute; intro C; inversion C.
      rewrite Habs. rewrite H. omega.
    apply Zlt_le_succ in Hup.
    apply Zlt_le_succ in Hlo. apply Zsucc_le_compat in Hlo.
    assert (C : (Z.succ (Z.succ 1) <= 2)%Z) by (apply (Zle_trans _ _ _ Hlo Hup)).
    compute in C. apply C. reflexivity.
  unfold Z.gt.
  remember (((z * z - 2) * (z * z - 2) ?= 0)%Z) as c. destruct c.
  - contradict Hne. apply Z.compare_eq_iff. auto.
  - unfold Z.ge in Hge. symmetry in Heqc. contradiction.
  - reflexivity.
Qed.

End Q27.

Module Q28.

Require Import Reals.

Require Import QArith.
Require Import Qreals.
Require Import Fourier.

Theorem PI_RGT_3_05 : (PI > 3 + 5/100)%R.
Proof.
  assert (Hineq : (sum_f_R0 (tg_alt PI_tg) (S (2 * 5)) <= PI / 4)%R).
    destruct PI_ineq with 5%nat. assumption.
  apply Rmult_le_compat_r with (r:=4%R) in Hineq.
  replace (PI / 4 * 4)%R with PI in Hineq by field.
  refine (Rlt_le_trans _ _ _ _ Hineq).
  simpl. unfold tg_alt. unfold PI_tg.
  replace ((-1)^0) with 1 by field;
  replace ((-1)^1) with (-1) by field;
  replace ((-1)^2) with 1 by field;
  replace ((-1)^3) with (-1) by field;
  replace ((-1)^4) with 1 by field;
  replace ((-1)^5) with (-1) by field;
  replace ((-1)^6) with 1 by field;
  replace ((-1)^7) with (-1) by field;
  replace ((-1)^8) with 1 by field;
  replace ((-1)^9) with (-1) by field;
  replace ((-1)^10) with 1 by field;
  replace ((-1)^11) with (-1) by field.
  simpl.
  replace (2 + 1) with 3 by field;
  replace (3 + 1) with 4 by field;
  replace (4 + 1) with 5 by field;
  replace (5 + 1) with 6 by field;
  replace (6 + 1) with 7 by field;
  replace (7 + 1) with 8 by field;
  replace (8 + 1) with 9 by field;
  replace (9 + 1) with 10 by field;
  replace (10 + 1) with 11 by field;
  replace (11 + 1) with 12 by field;
  replace (12 + 1) with 13 by field;
  replace (13 + 1) with 14 by field;
  replace (14 + 1) with 15 by field;
  replace (15 + 1) with 16 by field;
  replace (16 + 1) with 17 by field;
  replace (17 + 1) with 18 by field;
  replace (18 + 1) with 19 by field;
  replace (19 + 1) with 20 by field;
  replace (20 + 1) with 21 by field;
  replace (21 + 1) with 22 by field;
  replace (22 + 1) with 23 by field.
  rewrite Ropp_mult_distr_l_reverse; rewrite Ropp_mult_distr_l_reverse;
  rewrite Ropp_mult_distr_l_reverse; rewrite Ropp_mult_distr_l_reverse;
  rewrite Ropp_mult_distr_l_reverse; rewrite Ropp_mult_distr_l_reverse.
  rewrite Rmult_1_l; rewrite Rmult_1_l; rewrite Rmult_1_l; rewrite Rmult_1_l;
  rewrite Rmult_1_l; rewrite Rmult_1_l; rewrite Rmult_1_l; rewrite Rmult_1_l;
  rewrite Rmult_1_l; rewrite Rmult_1_l; rewrite Rmult_1_l; rewrite Rmult_1_l.
  replace 100    with (Q2R (100 # 1)) by (compute; field);
  replace (-/23) with (Q2R (-1 # 23)) by (compute; field);
  replace (/21)  with (Q2R ( 1 # 21)) by (compute; field);
  replace (-/19) with (Q2R (-1 # 19)) by (compute; field);
  replace (/17)  with (Q2R (1  # 17)) by (compute; field);
  replace (-/15) with (Q2R (-1 # 15)) by (compute; field);
  replace (/13)  with (Q2R (1  # 13)) by (compute; field);
  replace (-/11) with (Q2R (-1 # 11)) by (compute; field);
  replace (/9 )  with (Q2R (1  #  9)) by (compute; field);
  replace (-/7 ) with (Q2R (-1 #  7)) by (compute; field);
  replace (/5 )  with (Q2R (1  #  5)) by (compute; field);
  replace 5      with (Q2R (5  #  1)) by (compute; field);
  replace 4      with (Q2R (4  #  1)) by (compute; field);
  replace (-/3 ) with (Q2R (-1 #  3)) by (compute; field);
  replace 3      with (Q2R (3  #  1)) by (compute; field);
  replace (/2 )  with (Q2R (1  #  2)) by (compute; field);
  replace (-1)   with (Q2R (-1 #  1)) by (compute; field);
  replace (/1 )  with (Q2R (1  #  1)) by (compute; field).
  rewrite <- Q2R_div by (intro H; inversion H);
  rewrite <- Q2R_plus; rewrite <- Q2R_plus; rewrite <- Q2R_plus;
  rewrite <- Q2R_plus; rewrite <- Q2R_plus; rewrite <- Q2R_plus;
  rewrite <- Q2R_plus; rewrite <- Q2R_plus; rewrite <- Q2R_plus;
  rewrite <- Q2R_plus; rewrite <- Q2R_plus; rewrite <- Q2R_plus;
  rewrite <- Q2R_mult; apply Qlt_Rlt.
  compute. reflexivity.
  fourier.
Qed.

End Q28.