coq_practice_27.v

Require Import ZArith.

Lemma hoge : forall z : Z, (z ^ 4 - 4 * z ^ 2 + 4 > 0)%Z.
Proof.
  intros.
  assert (((z ^ 2 - 2)<>0)%Z -> (((z ^ 2 - 2)^2) > 0) % Z).
    intro.

    assert (forall p : Z, ((p<>0)%Z -> (p ^ 2 > 0) % Z)).
      intro.
      case p.
        intros.
        contradict H0.
        reflexivity.
        intros.
        simpl.
        reflexivity.
        intros.
        simpl.
        reflexivity.
    apply (H0 (z ^ 2 - 2)%Z).
    apply H.

  assert ((z * z <> 2)%Z).
    assert (forall p,Z.pos (p * p) <> 2%Z).
      simpl.
      destruct p.
      discriminate.
      destruct p.
      discriminate.
      discriminate.
      simpl.
      discriminate.
      simpl.
      discriminate.

    destruct z.
    simpl.
    discriminate.
    simpl.
    apply H0.
    simpl.
    apply H0.
    
  assert ((z ^ 4 - 4 * z ^ 2 + 4 = (z^2 - 2) ^ 2)%Z).
    ring.
    rewrite H1.

  apply H.
  intro.
  apply H0.
  rewrite Zplus_0_r_reverse.
  rewrite <- H2.
  ring.
Qed.