Require Import Nat Arith Lia.

Section Q.

Open Scope nat_scope.

Section StrongInduction.

  Variable P:nat -> Prop.

  Hypothesis IH : forall m, (forall n, n < m -> P n) -> P m.

  Lemma P0 : P 0.
  Proof.
    apply IH; intros.
    exfalso; inversion H.
  Qed.

  Hint Resolve P0.

  Lemma pred_increasing : forall n m,
      n <= m ->
      Nat.pred n <= Nat.pred m.
  Proof.
    induction n; cbn; intros.
    apply le_0_n.
    induction H; subst; cbn; eauto.
    destruct m; eauto.
  Qed.

  Hint Resolve le_S_n.

  Local Lemma strong_induction_all : forall n,
      (forall m, m <= n -> P m).
  Proof.
    induction n; intros;
      match goal with
      | [ H: _ <= _ |- _ ] =>
        inversion H
      end; eauto.
  Qed.

  Theorem strong_induction : forall n, P n.
  Proof.
    eauto using strong_induction_all.
  Qed.

End StrongInduction.

Tactic Notation "strong" "induction" ident(n) := induction n using strong_induction.

Lemma evenEx: forall (n : nat),
  Nat.even n = true -> exists x, 2 * x = n.
Proof.
  intros.
  strong induction n.
  destruct n.
  - exists 0; auto.
  - destruct n.
    + inversion H.
    + assert (exists x, 2 * x = n).
      { apply H0; auto. }
      inversion H1.
      exists (x + 1).
      lia.
Qed.

Lemma p: forall x y,
  0 < x -> 0 < y ->
  x * x <> 2 * y * y.
Proof.
  intros x.
  strong induction x.
  intros y Zx Zy contra.
  destruct (even x)eqn:EX.
  - destruct (even y)eqn:EY.
    + apply evenEx in EX.
      inversion EX.
      apply evenEx in EY.
      inversion EY.
      subst.
      assert (HC: x0 * x0 = 2 * x1 * x1).
      { lia. }
      assert (x0 * x0 <> 2 * x1 * x1).
      { apply H; lia. }
      auto.
    + apply evenEx in EX.
      inversion EX.
      subst.
      rewrite <- Nat.negb_odd in EY.
      apply Bool.negb_false_iff in EY.
      assert (HC: 2 * x0 * x0 = y * y).
      { lia. }
      assert (Nat.odd (y * y) = true).
      {
        rewrite Nat.odd_mul.
        intuition.
      }
      assert (Nat.odd (y * y) = false).
      {
        rewrite <- HC.
        apply Bool.negb_false_iff.
        replace (2 * x0 * x0) with (0 + 2 * (x0 * x0)) by lia.
        apply Nat.even_add_mul_2.
      }
      rewrite H0 in H1.
      inversion H1.
  - rewrite <- Nat.negb_odd in EX.
    apply Bool.negb_false_iff in EX.
    assert (Nat.odd (x * x) = true).
    {
      rewrite Nat.odd_mul.
      intuition.
    }
    assert (Nat.even (2 * y * y) = true).
    {
      rewrite Nat.even_mul.
      replace (2 * y) with (0 + 2 * y) by lia.
      rewrite Nat.even_add_mul_2.
      auto.
    }
    rewrite contra in H0.
    apply Bool.negb_false_iff in H1.
    rewrite Nat.negb_even in H1.
    rewrite H0 in H1.
    inversion H1.
Qed.


End Q.

Require Import Reals Lra.
Open Scope R_scope.

Lemma d: forall x y z,
  y <> 0 ->
    x / y = z -> x = z * y.
Proof.
  intros.
  subst.
  unfold Rdiv.
  rewrite Rmult_assoc.
  field.
  auto.
Qed.

Lemma sqrt2: forall x y,
  (0 < x)%nat -> (0 < y)%nat ->
    INR x / INR y <> sqrt 2.
Proof.
  intros x y Zx Zy contra.
  symmetry in contra.
  apply sqrt_lem_0 in contra.
  * replace (INR x / INR y * (INR x / INR y)) with
            (INR x * INR x / (INR y * INR y)) in *.
    rewrite <- mult_INR in contra.
    rewrite <- mult_INR in contra.
    apply d in contra.
    assert (HC: (x * x)%nat <> (2 * y * y)%nat).
    { apply p; auto. }
    apply not_INR in HC.
    replace (INR (2 * y * y)) with (2 * INR (y * y)) in HC.
    auto.
    symmetry.
    replace ((2 * y * y)%nat) with ((2 * (y * y))%nat) by lia.
    rewrite mult_INR.
    auto.
    apply not_0_INR.
    intros HC.
    inversion HC.
    destruct y.
    inversion Zy.
    inversion HC.
    field.
    apply not_0_INR.
    lia.
  * lra.
  * apply Rlt_le.
    apply Rdiv_lt_0_compat;
      replace 0 with (INR 0);
      try apply lt_INR; auto.
Qed.