task26.v

Require Import Omega.

Goal (221 * 293 * 389 * 397 + 17 = 14 * 119 * 127 * 151 * 313)%nat.
Proof.
  omega.
Qed.

task27.v

Require Import ZArith.
Require Import Omega.
Require Import Ring.

Lemma hoge : forall z : Z, (z ^ 4 - 4 * z ^ 2 + 4 > 0)%Z.
Proof.
  intros.
  replace (z^4 - 4*z^2 + 4)%Z with ((z^2-2)^2)%Z by ring.
  assert( z = -1 \/ z = 0 \/ z = 1 \/ z >= 2 \/ z <= -2 )%Z by omega.
  case H.
  intros.
  rewrite H0.
  replace ((-1)^2)%Z with 1%Z by ring.
  replace (1-2)%Z with (-1)%Z by ring.
  replace ((-1)^2)%Z with 1%Z by ring.
  reflexivity.
  intros.
  case H0.
  intros.
  rewrite H1.
  replace (0^2)%Z with 0%Z by ring.
  replace (0-2)%Z with (-2)%Z by ring.
  replace ((-2)^2)%Z with 4%Z by ring.
  omega.
  intros.
  destruct H1.
  rewrite H1.
  replace (1^2-2)%Z with (-1)%Z by ring.
  replace ((-1)^2)%Z with 1%Z by ring.
  omega.
  destruct H1.
  assert (2*z <= z*z)%Z.
  apply (Zmult_le_compat_r 2 z z).
  omega.
  omega.
  assert( 2 * 2 <= 2 * z )%Z.
  apply (Zmult_le_compat_l 2 z 2).
  omega.
  omega.
  assert (2 * 2 <= z * z)%Z.
  omega.
  assert (z*z = z^2)%Z by ring.
  assert (2*2 <= z^2)%Z.
  rewrite <- H5.
  apply H4.
  assert(z^2 - 2 >= 2)%Z.
  omega.
  assert( 2*(z^2-2) <= (z^2-2)*(z^2-2))%Z.
  apply (Zmult_le_compat_r 2 (z^2 -2) (z^2 -2)).
  omega.
  omega.
  assert( 2*2 <= 2*(z^2-2) )%Z.
  apply (Zmult_le_compat_l 2 (z^2-2) 2).
  omega.
  omega.
  assert (2*2 <= (z^2-2)*(z^2-2))%Z.
  omega.
  assert( (z^2-2)^2 = (z^2-2)*(z^2-2))%Z.
  ring.
  assert ((z^2-2)^2 >= 4)%Z.
  rewrite H11.
  omega.
  omega.
  assert( -z >= 2 )%Z by omega.
  assert( 2*(-z) <= (-z)*(-z) )%Z.
  apply (Zmult_le_compat_r 2 (-z) (-z)).
  omega.
  omega.
  assert( 2*2 <= 2*-z )%Z.
  apply (Zmult_le_compat_l 2 (-z) 2).
  omega.
  omega.
  assert (2*2 <= -z*-z)%Z.
  omega.
  assert( -z*-z = z^2 )%Z.
  ring.
  assert( 4 <= z^2 )%Z.
  omega.
  assert( z^2-2 >= 2 )%Z.
  omega.
  assert( 2*(z^2-2) <= (z^2-2)*(z^2-2))%Z.
  apply (Zmult_le_compat_r 2 (z^2-2) (z^2-2)).
  omega.
  omega.
  assert (2*2 <= 2*(z^2-2))%Z.
  apply (Zmult_le_compat_l 2 (z^2-2) 2).
  omega.
  omega.
  assert( 2*2 <= (z^2-2)*(z^2-2))%Z.
  omega.
  assert( (z^2-2)*(z^2-2)=(z^2-2)^2)%Z by ring.
  assert( 4 <= (z^2-2)^2 )%Z.
  rewrite <- H12.
  omega.
  omega.
Qed.