(*
* Coq 8.8.1
*)

Require Import Reals ZArith Omega.
Open Scope R_scope.

Lemma q: forall x y,
  x * x <> y * y -> x <> y.
Proof.
  intros x y H contra.
  rewrite contra in H.
  auto.
Qed.

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 w: forall x y,
  y <> 0 ->
    (x / y) * (x / y) = (x * x) / (y * y).
Proof.
  intros.
  field.
  auto.
Qed.

Lemma t: forall x y,
  exists z, x * y = z.
Proof.
  intros.
  exists (x * y).
  auto.
Qed.

Lemma a': IZR (1414213562370951 * 1414213562370951) <> IZR (2 * 1000000000000000 * 1000000000000000).
Proof.
  intros contra.
  apply eq_IZR in contra.
  omega.
Qed.

Lemma a: 1414213562370951 * 1414213562370951 <> 2 * 1000000000000000 * 1000000000000000.
Proof.
  intros contra.
  apply a'.
  repeat rewrite mult_IZR.
  auto.
Qed.

Lemma b: 1000000000000000 <> 0.
Proof.
  intros contra.
  apply eq_IZR in contra.
  omega.
Qed.


Lemma _42: 1414213562370951 / 1000000000000000 <> sqrt 2.
Proof.
  apply q.
  replace (sqrt 2 * sqrt 2) with 2.
  intros contra.
  remember 1414213562370951 as x.
  remember 1000000000000000 as y.
  rewrite w in contra.
  apply d with (x * x) (y * y) 2 in contra.
  subst.
  rewrite <- Rmult_assoc in contra.
  apply a.
  auto.

  apply Rmult_integral_contrapositive.
  split; subst; apply b.

  subst. apply b.
  rewrite sqrt_def; auto.
  apply Rlt_le.
  apply Rlt_0_2.
Qed.