(* Pythagorean.v *)

(***********************)
(* Pythagorean triples *)
(***********************)

Require Export Tactics.

(* A non nul predicate *)
Definition nnl_triple (a b c : Z) := ~(a = 0) /\ ~(b = 0) /\ ~(c = 0).

(* A positive predicate *)
Definition pos_triple (a b c : Z) := (a >= 0) /\ (b >= 0) /\ (c >= 0).

(* A Pythagorean predicate *)
Definition is_pytha (a b c : Z) := (pos_triple a b c) /\ a * a + b * b = c * c.

(* Unit circle and D_r *)
Definition in_ucirc (x y : R) := (x * x + y * y = 1)%R.
Definition D_r (r x y : R) := (y = r * (x + 1))%R.

(******************************)
(* Set of Pythagorean triples *)
(******************************)

(* step1 *)

Lemma pytha_ucirc1 : forall a b c : Z,
  (c > 0) -> (is_pytha a b c) -> (in_ucirc (frac a c) (frac b c)).
Proof.
(* Goal: forall (a b c : Z) (_ : Z.gt c Z0) (_ : is_pytha a b c), in_ucirc (frac a c) (frac b c) *)
  intros; unfold in_ucirc; unfold frac; field_simplify_eq.
(* Goal: @eq R (Rplus (pow (IZR a) (S (S O))) (pow (IZR b) (S (S O)))) (pow (IZR c) (S (S O))) *)
(* Goal: not (@eq R (IZR c) (IZR Z0)) *)
  unfold is_pytha in H0; elim H0; intros. 
(* Goal: @eq R (Rplus (pow (IZR a) (S (S O))) (pow (IZR b) (S (S O)))) (pow (IZR c) (S (S O))) *)
(* Goal: not (@eq R (IZR c) (IZR Z0)) *)
  repeat rewrite pow_IZR. rewrite <- plus_IZR. simpl Z_of_nat.
(* Goal: @eq R (IZR (Z.add (Z.pow a (Zpos (xO xH))) (Z.pow b (Zpos (xO xH))))) (IZR (Z.pow c (Zpos (xO xH)))) *)
(* Goal: not (@eq R (IZR c) (IZR Z0)) *)
  ring_simplify [(sym_eq H2)] (c^2);trivial.
(* Goal: not (@eq R (IZR c) (IZR Z0)) *)
(* Goal: not (@eq R (IZR (Z.mul c c)) (IZR Z0)) *)
(* Goal: not (@eq R (Rinv (Rmult (IZR c) (IZR c))) (IZR Z0)) *)
  discrR; auto with zarith.
Qed.

Lemma pytha_ucirc2 : forall a b c : Z, (a >= 0) /\ (b >= 0) /\ (c > 0) ->
  (in_ucirc (frac a c) (frac b c)) -> (is_pytha a b c).
Proof.
(* Goal: forall (a b c : Z) (_ : and (Z.ge a Z0) (and (Z.ge b Z0) (Z.gt c Z0))) (_ : in_ucirc (frac a c) (frac b c)), is_pytha a b c *)
  unfold in_ucirc; unfold frac; unfold is_pytha; intros; split.
(* Goal: pos_triple a b c *)
(* Goal: @eq Z (Z.add (Z.mul a a) (Z.mul b b)) (Z.mul c c) *)
  unfold pos_triple; auto with zarith.
(* Goal: @eq Z (Z.add (Z.mul a a) (Z.mul b b)) (Z.mul c c) *)
 apply eq_IZR; apply (Rmult_eq_reg_l (/ (IZR c * IZR c))).
(* Goal: @eq R (Rmult (Rinv (Rmult (IZR c) (IZR c))) (IZR (Z.add (Z.mul a a) (Z.mul b b)))) (Rmult (Rinv (Rmult (IZR c) (IZR c))) (IZR (Z.mul c c))) *)
(* Goal: not (@eq R (Rinv (Rmult (IZR c) (IZR c))) (IZR Z0)) *)
 pattern (IZR c * IZR c)%R at 2; rewrite <- mult_IZR;rewrite Rinv_l.
(* Goal: @eq R (Rmult (Rinv (Rmult (IZR c) (IZR c))) (IZR (Z.add (Z.mul a a) (Z.mul b b)))) (IZR (Zpos xH)) *)
(* Goal: not (@eq R (IZR (Z.mul c c)) (IZR Z0)) *)
(* Goal: not (@eq R (Rinv (Rmult (IZR c) (IZR c))) (IZR Z0)) *)
 rewrite Rinv_mult_distr.
(* Goal: @eq R (Rmult (Rmult (Rinv (IZR c)) (Rinv (IZR c))) (IZR (Z.add (Z.mul a a) (Z.mul b b)))) (IZR (Zpos xH)) *)
(* Goal: not (@eq R (IZR c) (IZR Z0)) *)
(* Goal: not (@eq R (IZR c) (IZR Z0)) *)
(* Goal: not (@eq R (IZR (Z.mul c c)) (IZR Z0)) *)
(* Goal: not (@eq R (Rinv (Rmult (IZR c) (IZR c))) (IZR Z0)) *)
 rewrite <- H0; rewrite plus_IZR; repeat rewrite mult_IZR; field.
(* Goal: not (@eq R (IZR c) (IZR Z0)) *)
(* Goal: not (@eq R (IZR (Z.mul c c)) (IZR Z0)) *)
(* Goal: not (@eq R (Rinv (Rmult (IZR c) (IZR c))) (IZR Z0)) *)
 discrR; auto with zarith.
(* Goal: not (@eq R (IZR c) (IZR Z0)) *)
(* Goal: not (@eq R (IZR (Z.mul c c)) (IZR Z0)) *)
(* Goal: not (@eq R (Rinv (Rmult (IZR c) (IZR c))) (IZR Z0)) *)
 discrR; auto with zarith.
(* Goal: not (@eq R (IZR c) (IZR Z0)) *)
(* Goal: not (@eq R (IZR (Z.mul c c)) (IZR Z0)) *)
(* Goal: not (@eq R (Rinv (Rmult (IZR c) (IZR c))) (IZR Z0)) *)
 discrR; auto with zarith.
(* Goal: not (@eq R (IZR c) (IZR Z0)) *)
(* Goal: not (@eq R (IZR (Z.mul c c)) (IZR Z0)) *)
(* Goal: not (@eq R (Rinv (Rmult (IZR c) (IZR c))) (IZR Z0)) *)
 rewrite mult_IZR; split_Rmult; discrR; auto with zarith.
(* Goal: not (@eq R (IZR c) (IZR Z0)) *)
(* Goal: not (@eq R (IZR (Z.mul c c)) (IZR Z0)) *)
(* Goal: not (@eq R (Rinv (Rmult (IZR c) (IZR c))) (IZR Z0)) *)
 apply Rinv_neq_0_compat; split_Rmult; discrR; auto with zarith.
Qed.

(* step 2 *)

(* Intersection between the unit circle and D_r *)
Definition interCDr (r x y : R) := (in_ucirc x y) /\ (D_r r x y).

(* Points of the intersection *)
Definition p1 := (-1,0)%R.
Definition p2 (r : R) :=
  let den := (1 + r * r)%R in
  ((1 - r * r) / den, 2 * r / den)%R.

(* Equality over points *)
Definition eqp (p1 p2 : R * R) := (fst p1) = (fst p2) /\ (snd p1)= (snd p2).

(* Total order over points (using R) *)
Lemma ordp : forall p1 p2 : R * R, (eqp p1 p2) \/ ~(eqp p1 p2).
Proof.
(* Goal: forall p1 p2 : prod R R, or (eqp p1 p2) (not (eqp p1 p2)) *)
  intros p3 p4. unfold eqp; elim p3; elim p4; intros; simpl.
(* Goal: or (and (@eq R a0 a) (@eq R b0 b)) (not (and (@eq R a0 a) (@eq R b0 b))) *)
  elim (Req_dec a a0); elim (Req_dec b b0); intuition.
Qed.

(* Characterization of the intersection *)
Lemma interCDr_sol : forall r x y : R,
  (interCDr r x y) -> (eqp (x,y) p1) \/ (eqp (x,y) (p2 r)).
Proof.
(* Goal: forall (r x y : R) (_ : interCDr r x y), or (eqp (@pair R R x y) p1) (eqp (@pair R R x y) (p2 r)) *)
  unfold interCDr;unfold in_ucirc;unfold D_r;unfold eqp, p1, p2;simpl.
(* Goal: forall (r x y : R) (_ : and (@eq R (Rplus (Rmult x x) (Rmult y y)) (IZR (Zpos xH))) (@eq R y (Rmult r (Rplus x (IZR (Zpos xH)))))), or (and (@eq R x (IZR (Zneg xH))) (@eq R y (IZR Z0))) (and (@eq R x (Rdiv (Rminus (IZR (Zpos xH)) (Rmult r r)) (Rplus (IZR (Zpos xH)) (Rmult r r)))) (@eq R y (Rdiv (Rmult (IZR (Zpos (xO xH))) r) (Rplus (IZR (Zpos xH)) (Rmult r r))))) *)
  intros;elim H;intros;rewrite H1 in H0.
(* Goal: or (and (@eq R x (IZR (Zneg xH))) (@eq R y (IZR Z0))) (and (@eq R x (Rdiv (Rminus (IZR (Zpos xH)) (Rmult r r)) (Rplus (IZR (Zpos xH)) (Rmult r r)))) (@eq R y (Rdiv (Rmult (IZR (Zpos (xO xH))) r) (Rplus (IZR (Zpos xH)) (Rmult r r))))) *)
  cut (((1 + r * r) * Rsqr x + 2 * r * r * x + (r * r - 1)) = 0)%R.
(* Goal: forall _ : @eq R (Rplus (Rplus (Rmult (Rplus (IZR (Zpos xH)) (Rmult r r)) (Rsqr x)) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) x)) (Rminus (Rmult r r) (IZR (Zpos xH)))) (IZR Z0), or (and (@eq R x (IZR (Zneg xH))) (@eq R y (IZR Z0))) (and (@eq R x (Rdiv (Rminus (IZR (Zpos xH)) (Rmult r r)) (Rplus (IZR (Zpos xH)) (Rmult r r)))) (@eq R y (Rdiv (Rmult (IZR (Zpos (xO xH))) r) (Rplus (IZR (Zpos xH)) (Rmult r r))))) *)
(* Goal: @eq R (Rplus (Rplus (Rmult (Rplus (IZR (Zpos xH)) (Rmult r r)) (Rsqr x)) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) x)) (Rminus (Rmult r r) (IZR (Zpos xH)))) (IZR Z0) *)
  intro;cut ((1 + r * r) <> 0)%R.
  intro;cut (Delta_is_pos (mknonzeroreal (1 + r * r) H3) (2 * r * r)
            (r * r - 1))%R.
  intro;generalize (Rsqr_sol_eq_0_0 (mknonzeroreal (1 + r * r) H3) (2 * r * r)
                                    (r * r - 1) x H4 H2)%R.
(* Goal: forall _ : or (@eq R x (sol_x1 (mknonzeroreal (Rplus (IZR (Zpos xH)) (Rmult r r)) H3) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rminus (Rmult r r) (IZR (Zpos xH))))) (@eq R x (sol_x2 (mknonzeroreal (Rplus (IZR (Zpos xH)) (Rmult r r)) H3) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rminus (Rmult r r) (IZR (Zpos xH))))), or (and (@eq R x (IZR (Zneg xH))) (@eq R y (IZR Z0))) (and (@eq R x (Rdiv (Rminus (IZR (Zpos xH)) (Rmult r r)) (Rplus (IZR (Zpos xH)) (Rmult r r)))) (@eq R y (Rdiv (Rmult (IZR (Zpos (xO xH))) r) (Rplus (IZR (Zpos xH)) (Rmult r r))))) *)
(* Goal: Delta_is_pos (mknonzeroreal (Rplus (IZR (Zpos xH)) (Rmult r r)) H3) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rminus (Rmult r r) (IZR (Zpos xH))) *)
(* Goal: not (@eq R (Rplus (IZR (Zpos xH)) (Rmult r r)) (IZR Z0)) *)
(* Goal: @eq R (Rplus (Rplus (Rmult (Rplus (IZR (Zpos xH)) (Rmult r r)) (Rsqr x)) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) x)) (Rminus (Rmult r r) (IZR (Zpos xH)))) (IZR Z0) *)
  unfold sol_x1, sol_x2;unfold Delta;unfold Rsqr;simpl.
(* Goal: forall _ : or (@eq R x (Rdiv (Rplus (Ropp (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (sqrt (Rminus (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (Rmult (Rmult (IZR (Zpos (xO (xO xH)))) (Rplus (IZR (Zpos xH)) (Rmult r r))) (Rminus (Rmult r r) (IZR (Zpos xH))))))) (Rmult (IZR (Zpos (xO xH))) (Rplus (IZR (Zpos xH)) (Rmult r r))))) (@eq R x (Rdiv (Rminus (Ropp (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (sqrt (Rminus (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (Rmult (Rmult (IZR (Zpos (xO (xO xH)))) (Rplus (IZR (Zpos xH)) (Rmult r r))) (Rminus (Rmult r r) (IZR (Zpos xH))))))) (Rmult (IZR (Zpos (xO xH))) (Rplus (IZR (Zpos xH)) (Rmult r r))))), or (and (@eq R x (IZR (Zneg xH))) (@eq R y (IZR Z0))) (and (@eq R x (Rdiv (Rminus (IZR (Zpos xH)) (Rmult r r)) (Rplus (IZR (Zpos xH)) (Rmult r r)))) (@eq R y (Rdiv (Rmult (IZR (Zpos (xO xH))) r) (Rplus (IZR (Zpos xH)) (Rmult r r))))) *)
(* Goal: Delta_is_pos (mknonzeroreal (Rplus (IZR (Zpos xH)) (Rmult r r)) H3) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rminus (Rmult r r) (IZR (Zpos xH))) *)
(* Goal: not (@eq R (Rplus (IZR (Zpos xH)) (Rmult r r)) (IZR Z0)) *)
(* Goal: @eq R (Rplus (Rplus (Rmult (Rplus (IZR (Zpos xH)) (Rmult r r)) (Rsqr x)) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) x)) (Rminus (Rmult r r) (IZR (Zpos xH)))) (IZR Z0) *)
  cut ((2 * r * r * (2 * r * r) - 4 * (1 + r * r) * (r * r - 1))%R = 4%R).
(* Goal: forall (_ : @eq R (Rminus (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (Rmult (Rmult (IZR (Zpos (xO (xO xH)))) (Rplus (IZR (Zpos xH)) (Rmult r r))) (Rminus (Rmult r r) (IZR (Zpos xH))))) (IZR (Zpos (xO (xO xH))))) (_ : or (@eq R x (Rdiv (Rplus (Ropp (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (sqrt (Rminus (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (Rmult (Rmult (IZR (Zpos (xO (xO xH)))) (Rplus (IZR (Zpos xH)) (Rmult r r))) (Rminus (Rmult r r) (IZR (Zpos xH))))))) (Rmult (IZR (Zpos (xO xH))) (Rplus (IZR (Zpos xH)) (Rmult r r))))) (@eq R x (Rdiv (Rminus (Ropp (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (sqrt (Rminus (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (Rmult (Rmult (IZR (Zpos (xO (xO xH)))) (Rplus (IZR (Zpos xH)) (Rmult r r))) (Rminus (Rmult r r) (IZR (Zpos xH))))))) (Rmult (IZR (Zpos (xO xH))) (Rplus (IZR (Zpos xH)) (Rmult r r)))))), or (and (@eq R x (IZR (Zneg xH))) (@eq R y (IZR Z0))) (and (@eq R x (Rdiv (Rminus (IZR (Zpos xH)) (Rmult r r)) (Rplus (IZR (Zpos xH)) (Rmult r r)))) (@eq R y (Rdiv (Rmult (IZR (Zpos (xO xH))) r) (Rplus (IZR (Zpos xH)) (Rmult r r))))) *)
(* Goal: @eq R (Rminus (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (Rmult (Rmult (IZR (Zpos (xO (xO xH)))) (Rplus (IZR (Zpos xH)) (Rmult r r))) (Rminus (Rmult r r) (IZR (Zpos xH))))) (IZR (Zpos (xO (xO xH)))) *)
(* Goal: Delta_is_pos (mknonzeroreal (Rplus (IZR (Zpos xH)) (Rmult r r)) H3) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rminus (Rmult r r) (IZR (Zpos xH))) *)
(* Goal: not (@eq R (Rplus (IZR (Zpos xH)) (Rmult r r)) (IZR Z0)) *)
(* Goal: @eq R (Rplus (Rplus (Rmult (Rplus (IZR (Zpos xH)) (Rmult r r)) (Rsqr x)) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) x)) (Rminus (Rmult r r) (IZR (Zpos xH)))) (IZR Z0) *)
  intro;rewrite H5. replace (4)%R with (2*2)%R by auto.
(* Goal: forall _ : or (@eq R x (Rdiv (Rplus (Ropp (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (sqrt (Rmult (IZR (Zpos (xO xH))) (IZR (Zpos (xO xH)))))) (Rmult (IZR (Zpos (xO xH))) (Rplus (IZR (Zpos xH)) (Rmult r r))))) (@eq R x (Rdiv (Rminus (Ropp (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (sqrt (Rmult (IZR (Zpos (xO xH))) (IZR (Zpos (xO xH)))))) (Rmult (IZR (Zpos (xO xH))) (Rplus (IZR (Zpos xH)) (Rmult r r))))), or (and (@eq R x (IZR (Zneg xH))) (@eq R y (IZR Z0))) (and (@eq R x (Rdiv (Rminus (IZR (Zpos xH)) (Rmult r r)) (Rplus (IZR (Zpos xH)) (Rmult r r)))) (@eq R y (Rdiv (Rmult (IZR (Zpos (xO xH))) r) (Rplus (IZR (Zpos xH)) (Rmult r r))))) *)
(* Goal: @eq R (Rminus (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (Rmult (Rmult (IZR (Zpos (xO (xO xH)))) (Rplus (IZR (Zpos xH)) (Rmult r r))) (Rminus (Rmult r r) (IZR (Zpos xH))))) (IZR (Zpos (xO (xO xH)))) *)
(* Goal: Delta_is_pos (mknonzeroreal (Rplus (IZR (Zpos xH)) (Rmult r r)) H3) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rminus (Rmult r r) (IZR (Zpos xH))) *)
(* Goal: not (@eq R (Rplus (IZR (Zpos xH)) (Rmult r r)) (IZR Z0)) *)
(* Goal: @eq R (Rplus (Rplus (Rmult (Rplus (IZR (Zpos xH)) (Rmult r r)) (Rsqr x)) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) x)) (Rminus (Rmult r r) (IZR (Zpos xH)))) (IZR Z0) *)
  rewrite sqrt_square.
(* Goal: forall _ : or (@eq R x (Rdiv (Rplus (Ropp (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (IZR (Zpos (xO xH)))) (Rmult (IZR (Zpos (xO xH))) (Rplus (IZR (Zpos xH)) (Rmult r r))))) (@eq R x (Rdiv (Rminus (Ropp (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (IZR (Zpos (xO xH)))) (Rmult (IZR (Zpos (xO xH))) (Rplus (IZR (Zpos xH)) (Rmult r r))))), or (and (@eq R x (IZR (Zneg xH))) (@eq R y (IZR Z0))) (and (@eq R x (Rdiv (Rminus (IZR (Zpos xH)) (Rmult r r)) (Rplus (IZR (Zpos xH)) (Rmult r r)))) (@eq R y (Rdiv (Rmult (IZR (Zpos (xO xH))) r) (Rplus (IZR (Zpos xH)) (Rmult r r))))) *)
(* Goal: Rle (IZR Z0) (IZR (Zpos (xO xH))) *)
(* Goal: @eq R (Rminus (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (Rmult (Rmult (IZR (Zpos (xO (xO xH)))) (Rplus (IZR (Zpos xH)) (Rmult r r))) (Rminus (Rmult r r) (IZR (Zpos xH))))) (IZR (Zpos (xO (xO xH)))) *)
(* Goal: Delta_is_pos (mknonzeroreal (Rplus (IZR (Zpos xH)) (Rmult r r)) H3) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rminus (Rmult r r) (IZR (Zpos xH))) *)
(* Goal: not (@eq R (Rplus (IZR (Zpos xH)) (Rmult r r)) (IZR Z0)) *)
(* Goal: @eq R (Rplus (Rplus (Rmult (Rplus (IZR (Zpos xH)) (Rmult r r)) (Rsqr x)) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) x)) (Rminus (Rmult r r) (IZR (Zpos xH)))) (IZR Z0) *)
  induction 1;[right|left].
  split;[rewrite H6;field;assumption
        |rewrite H1;rewrite H6;field;assumption].
  split;[rewrite H6;field;assumption
        |rewrite H1;rewrite H6;field;assumption].
(* Goal: Rle (IZR Z0) (IZR (Zpos (xO xH))) *)
(* Goal: @eq R (Rminus (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (Rmult (Rmult (IZR (Zpos (xO (xO xH)))) (Rplus (IZR (Zpos xH)) (Rmult r r))) (Rminus (Rmult r r) (IZR (Zpos xH))))) (IZR (Zpos (xO (xO xH)))) *)
(* Goal: Delta_is_pos (mknonzeroreal (Rplus (IZR (Zpos xH)) (Rmult r r)) H3) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rminus (Rmult r r) (IZR (Zpos xH))) *)
(* Goal: not (@eq R (Rplus (IZR (Zpos xH)) (Rmult r r)) (IZR Z0)) *)
(* Goal: @eq R (Rplus (Rplus (Rmult (Rplus (IZR (Zpos xH)) (Rmult r r)) (Rsqr x)) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) x)) (Rminus (Rmult r r) (IZR (Zpos xH)))) (IZR Z0) *)
  unfold Rle;left;prove_sup.
(* Goal: @eq R (Rminus (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (Rmult (Rmult (IZR (Zpos (xO (xO xH)))) (Rplus (IZR (Zpos xH)) (Rmult r r))) (Rminus (Rmult r r) (IZR (Zpos xH))))) (IZR (Zpos (xO (xO xH)))) *)
(* Goal: Delta_is_pos (mknonzeroreal (Rplus (IZR (Zpos xH)) (Rmult r r)) H3) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rminus (Rmult r r) (IZR (Zpos xH))) *)
(* Goal: not (@eq R (Rplus (IZR (Zpos xH)) (Rmult r r)) (IZR Z0)) *)
(* Goal: @eq R (Rplus (Rplus (Rmult (Rplus (IZR (Zpos xH)) (Rmult r r)) (Rsqr x)) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) x)) (Rminus (Rmult r r) (IZR (Zpos xH)))) (IZR Z0) *)
  ring.
  unfold Delta_is_pos;unfold Delta;unfold Rsqr;simpl;
    ring_simplify (2 * r * r * (2 * r * r) - 4 * (1 + r * r) * (r * r - 1))%R;
(* Goal: Rle (IZR Z0) (IZR (Zpos (xO xH))) *)
(* Goal: @eq R (Rminus (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (Rmult (Rmult (IZR (Zpos (xO (xO xH)))) (Rplus (IZR (Zpos xH)) (Rmult r r))) (Rminus (Rmult r r) (IZR (Zpos xH))))) (IZR (Zpos (xO (xO xH)))) *)
(* Goal: Delta_is_pos (mknonzeroreal (Rplus (IZR (Zpos xH)) (Rmult r r)) H3) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rminus (Rmult r r) (IZR (Zpos xH))) *)
(* Goal: not (@eq R (Rplus (IZR (Zpos xH)) (Rmult r r)) (IZR Z0)) *)
(* Goal: @eq R (Rplus (Rplus (Rmult (Rplus (IZR (Zpos xH)) (Rmult r r)) (Rsqr x)) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) x)) (Rminus (Rmult r r) (IZR (Zpos xH)))) (IZR Z0) *)
    unfold Rle;left;prove_sup.
  apply Rgt_not_eq;unfold Rgt;rewrite Rplus_comm;apply Rle_lt_0_plus_1;
    fold (Rsqr r);elim (Req_dec r 0);intro;
    [rewrite H3;rewrite Rsqr_0;unfold Rle;right;auto
    |unfold Rle;left;apply Rsqr_pos_lt;assumption].
(* Goal: @eq R (Rminus (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (Rmult (Rmult (IZR (Zpos (xO (xO xH)))) (Rplus (IZR (Zpos xH)) (Rmult r r))) (Rminus (Rmult r r) (IZR (Zpos xH))))) (IZR (Zpos (xO (xO xH)))) *)
(* Goal: Delta_is_pos (mknonzeroreal (Rplus (IZR (Zpos xH)) (Rmult r r)) H3) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rminus (Rmult r r) (IZR (Zpos xH))) *)
(* Goal: not (@eq R (Rplus (IZR (Zpos xH)) (Rmult r r)) (IZR Z0)) *)
(* Goal: @eq R (Rplus (Rplus (Rmult (Rplus (IZR (Zpos xH)) (Rmult r r)) (Rsqr x)) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) x)) (Rminus (Rmult r r) (IZR (Zpos xH)))) (IZR Z0) *)
  pattern 1%R at 2;rewrite <- H0;unfold Rsqr;ring.
Qed.

(* step 3 *)

Lemma rat_coo1 : forall x y : R, (in_ucirc x y) /\
  (exists r : R, (is_rat r) /\ (interCDr r x y)) -> (is_ratp (x,y)).
Proof.
(* Goal: forall (x y : R) (_ : and (in_ucirc x y) (@ex R (fun r : R => and (is_rat r) (interCDr r x y)))), is_ratp (@pair R R x y) *)
  unfold in_ucirc, is_ratp, is_rat.
  unfold frac; intros; elim H; intros; elim H1; intros; elim H2; intros;
    elim H3; intro; elim x1;intros; elim H5; intros;
    elim (interCDr_sol x0 x y H4); unfold eqp, p1, p2; simpl; intro; elim H8;
    intros; rewrite H9; rewrite H10.
(* Goal: and (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) (Rdiv (IZR a) (IZR b))) (Rplus (IZR (Zpos xH)) (Rmult (Rdiv (IZR a) (IZR b)) (Rdiv (IZR a) (IZR b))))) (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR a)) (IZR b)) (Rplus (Rmult (IZR a) (IZR a)) (Rmult (IZR b) (IZR b))))) (and (Z.ge a Z0) (and (Z.gt b Z0) (and (Z.le a b) (rel_prime a b)))) *)
  split.
(* Goal: @ex (prod Z Z) (fun pq : prod Z Z => let (p, q) := pq in and (not (@eq Z q Z0)) (@eq R (IZR (Zneg xH)) (Rdiv (IZR p) (IZR q)))) *)
(* Goal: @ex (prod Z Z) (fun pq : prod Z Z => let (p, q) := pq in and (not (@eq Z q Z0)) (@eq R (IZR Z0) (Rdiv (IZR p) (IZR q)))) *)
(* Goal: and (@ex (prod Z Z) (fun pq : prod Z Z => let (p, q) := pq in and (not (@eq Z q Z0)) (@eq R (Rdiv (Rminus (IZR (Zpos xH)) (Rmult x0 x0)) (Rplus (IZR (Zpos xH)) (Rmult x0 x0))) (Rdiv (IZR p) (IZR q))))) (@ex (prod Z Z) (fun pq : prod Z Z => let (p, q) := pq in and (not (@eq Z q Z0)) (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) x0) (Rplus (IZR (Zpos xH)) (Rmult x0 x0))) (Rdiv (IZR p) (IZR q))))) *)
  exists (-1,1); split; [ auto with zarith | simpl; field; discrR ].
(* Goal: @ex (prod Z Z) (fun pq : prod Z Z => let (p, q) := pq in and (not (@eq Z q Z0)) (@eq R (IZR Z0) (Rdiv (IZR p) (IZR q)))) *)
(* Goal: and (@ex (prod Z Z) (fun pq : prod Z Z => let (p, q) := pq in and (not (@eq Z q Z0)) (@eq R (Rdiv (Rminus (IZR (Zpos xH)) (Rmult x0 x0)) (Rplus (IZR (Zpos xH)) (Rmult x0 x0))) (Rdiv (IZR p) (IZR q))))) (@ex (prod Z Z) (fun pq : prod Z Z => let (p, q) := pq in and (not (@eq Z q Z0)) (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) x0) (Rplus (IZR (Zpos xH)) (Rmult x0 x0))) (Rdiv (IZR p) (IZR q))))) *)
  exists (0,1); split; [ auto with zarith | simpl; field; discrR ].
(* Goal: and (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) (Rdiv (IZR a) (IZR b))) (Rplus (IZR (Zpos xH)) (Rmult (Rdiv (IZR a) (IZR b)) (Rdiv (IZR a) (IZR b))))) (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR a)) (IZR b)) (Rplus (Rmult (IZR a) (IZR a)) (Rmult (IZR b) (IZR b))))) (and (Z.ge a Z0) (and (Z.gt b Z0) (and (Z.le a b) (rel_prime a b)))) *)
  split.
(* Goal: and (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) (Rdiv (IZR a) (IZR b))) (Rplus (IZR (Zpos xH)) (Rmult (Rdiv (IZR a) (IZR b)) (Rdiv (IZR a) (IZR b))))) (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR a)) (IZR b)) (Rplus (Rmult (IZR a) (IZR a)) (Rmult (IZR b) (IZR b))))) (and (Z.ge a Z0) (and (Z.gt b Z0) (and (Z.le a b) (rel_prime a b)))) *)
  exists (b * b - a * a, a * a + b * b); split.
(* Goal: not (@eq Z (Z.add (Z.mul a a) (Z.mul b b)) Z0) *)
(* Goal: @eq R (Rdiv (Rminus (IZR (Zpos xH)) (Rmult x0 x0)) (Rplus (IZR (Zpos xH)) (Rmult x0 x0))) (Rdiv (IZR (Z.sub (Z.mul b b) (Z.mul a a))) (IZR (Z.add (Z.mul a a) (Z.mul b b)))) *)
(* Goal: @ex (prod Z Z) (fun pq : prod Z Z => let (p, q) := pq in and (not (@eq Z q Z0)) (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) x0) (Rplus (IZR (Zpos xH)) (Rmult x0 x0))) (Rdiv (IZR p) (IZR q)))) *)
  auto with zarith.
  rewrite H7; rewrite <- Z_R_minus; rewrite plus_IZR; repeat rewrite mult_IZR;
    field; split;discrR; auto with zarith reals.
(* Goal: and (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) (Rdiv (IZR a) (IZR b))) (Rplus (IZR (Zpos xH)) (Rmult (Rdiv (IZR a) (IZR b)) (Rdiv (IZR a) (IZR b))))) (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR a)) (IZR b)) (Rplus (Rmult (IZR a) (IZR a)) (Rmult (IZR b) (IZR b))))) (and (Z.ge a Z0) (and (Z.gt b Z0) (and (Z.le a b) (rel_prime a b)))) *)
  exists (2 * a * b * b, (a * a + b * b) * b); split.
(* Goal: not (@eq R (IZR c) (IZR Z0)) *)
(* Goal: not (@eq R (IZR (Z.mul c c)) (IZR Z0)) *)
(* Goal: not (@eq R (Rinv (Rmult (IZR c) (IZR c))) (IZR Z0)) *)
  apply not_IZR_0; rewrite mult_IZR; split_Rmult; discrR; auto with zarith.
  rewrite H7; repeat rewrite mult_IZR; rewrite plus_IZR;
    repeat rewrite mult_IZR; simpl; field; split; discrR;
    auto with zarith reals.
Qed.

Lemma rat_coo2 : forall x y : R, (in_ucirc x y) /\ (is_ratp (x,y)) ->
  exists r : R, (is_rat r) /\ (interCDr r x y).
Proof.
(* Goal: forall (x y : R) (_ : and (in_ucirc x y) (is_ratp (@pair R R x y))), @ex R (fun r : R => and (is_rat r) (interCDr r x y)) *)
  unfold in_ucirc, is_ratp, is_rat, interCDr.
(* Goal: forall (x y : R) (_ : and (@eq R (Rplus (Rmult x x) (Rmult y y)) (IZR (Zpos xH))) (and (@ex (prod Z Z) (fun pq : prod Z Z => let (p, q) := pq in and (not (@eq Z q Z0)) (@eq R x (frac p q)))) (@ex (prod Z Z) (fun pq : prod Z Z => let (p, q) := pq in and (not (@eq Z q Z0)) (@eq R y (frac p q)))))), @ex R (fun r : R => and (@ex (prod Z Z) (fun pq : prod Z Z => let (p, q) := pq in and (not (@eq Z q Z0)) (@eq R r (frac p q)))) (and (in_ucirc x y) (D_r r x y))) *)
  unfold frac, in_ucirc, D_r; intros.
(* Goal: @ex R (fun r : R => and (@ex (prod Z Z) (fun pq : prod Z Z => let (p, q) := pq in and (not (@eq Z q Z0)) (@eq R r (Rdiv (IZR p) (IZR q))))) (and (@eq R (Rplus (Rmult x x) (Rmult y y)) (IZR (Zpos xH))) (@eq R y (Rmult r (Rplus x (IZR (Zpos xH))))))) *)
  elim (Req_dec x (-1)%R); intro.
(* Goal: and (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) (Rdiv (IZR a) (IZR b))) (Rplus (IZR (Zpos xH)) (Rmult (Rdiv (IZR a) (IZR b)) (Rdiv (IZR a) (IZR b))))) (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR a)) (IZR b)) (Rplus (Rmult (IZR a) (IZR a)) (Rmult (IZR b) (IZR b))))) (and (Z.ge a Z0) (and (Z.gt b Z0) (and (Z.le a b) (rel_prime a b)))) *)
  exists 1%R; split.
(* Goal: @ex (prod Z Z) (fun pq : prod Z Z => let (p, q) := pq in and (not (@eq Z q Z0)) (@eq R (IZR (Zpos xH)) (Rdiv (IZR p) (IZR q)))) *)
(* Goal: and (@eq R (Rplus (Rmult x x) (Rmult y y)) (IZR (Zpos xH))) (@eq R y (Rmult (IZR (Zpos xH)) (Rplus x (IZR (Zpos xH))))) *)
(* Goal: @ex R (fun r : R => and (@ex (prod Z Z) (fun pq : prod Z Z => let (p, q) := pq in and (not (@eq Z q Z0)) (@eq R r (Rdiv (IZR p) (IZR q))))) (and (@eq R (Rplus (Rmult x x) (Rmult y y)) (IZR (Zpos xH))) (@eq R y (Rmult r (Rplus x (IZR (Zpos xH))))))) *)
  exists (1,1); split; [ auto with zarith | field; discrR ].
(* Goal: and (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) (Rdiv (IZR a) (IZR b))) (Rplus (IZR (Zpos xH)) (Rmult (Rdiv (IZR a) (IZR b)) (Rdiv (IZR a) (IZR b))))) (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR a)) (IZR b)) (Rplus (Rmult (IZR a) (IZR a)) (Rmult (IZR b) (IZR b))))) (and (Z.ge a Z0) (and (Z.gt b Z0) (and (Z.le a b) (rel_prime a b)))) *)
  elim H; intros; split.
(* Goal: interCDr x0 x y *)
  assumption.
  rewrite H0; rewrite H0 in H1; ring_simplify (1 * (-1 + 1))%R;
    cut ((1 + y * y) = 1)%R;
    [ intro; apply Rsqr_0_uniq; unfold Rsqr;
      apply (Rplus_0_r_uniq 1 (y * y) H3)%R
    | pattern 1%R at 2; rewrite <- H1; ring ].
  exists (y / (x + 1))%R; cut ((x + 1) <> 0)%R;
    [ intro; split
    | rewrite <- (Ropp_involutive 1); fold (x - -1)%R; apply Rminus_eq_contra;
      assumption ].
  elim H; intros; elim H3; intros; elim H4; intro; elim x0; intros; elim H6;
    intros; elim H5; intro; elim x1; intros; elim H9; intros; rewrite H8;
    rewrite H11.
  cut (a + b <> 0);
    [ intro
    | apply not_IZR_0;
      cut (((IZR a / IZR b + 1) * IZR b)%R = (IZR a + IZR b)%R);
        [ intro; rewrite plus_IZR; rewrite <- H12; split_Rmult;
          [ rewrite <- H8; assumption
          | discrR; assumption ]
        | field; discrR; assumption ] ].
(* Goal: and (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) (Rdiv (IZR a) (IZR b))) (Rplus (IZR (Zpos xH)) (Rmult (Rdiv (IZR a) (IZR b)) (Rdiv (IZR a) (IZR b))))) (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR a)) (IZR b)) (Rplus (Rmult (IZR a) (IZR a)) (Rmult (IZR b) (IZR b))))) (and (Z.ge a Z0) (and (Z.gt b Z0) (and (Z.le a b) (rel_prime a b)))) *)
  exists (a0 * b, b0 * (a + b)); split.
  apply not_IZR_0; rewrite mult_IZR; rewrite plus_IZR; split_Rmult; discrR;
(* Goal: interCDr x0 x y *)
    assumption.
(* Goal: interCDr x0 x y *)
  repeat rewrite mult_IZR; rewrite plus_IZR; field; discrR; try assumption.
  repeat split; discrR; try assumption; fold (IZR a / IZR b)%R;
(* Goal: interCDr x0 x y *)
    rewrite <- H8; assumption.
(* Goal: and (@eq R (Rplus (Rmult x x) (Rmult y y)) (IZR (Zpos xH))) (@eq R y (Rmult (Rdiv y (Rplus x (IZR (Zpos xH)))) (Rplus x (IZR (Zpos xH))))) *)
  split; [ elim H; intros; assumption | field; assumption ].
Qed.

(* step 4 *)

(* Positivity predicate over points *)
Definition is_posp (c : R * R) := (fst c >= 0)%R /\ (snd c >= 0)%R.

(* Predicate for the positive rational coordinates of the unit circle *)
Definition is_ucp (c : R * R) :=
  (in_ucirc (fst c) (snd c)) /\ (is_ratp c) /\ (is_posp c).

(* Positive rational coordinates of the unit circle *)
Definition ucp (p q : Z) :=
  let pr := (IZR p) in
  let qr := (IZR q) in
  let den := (pr * pr + qr * qr)%R in
  ((qr * qr - pr * pr) / den, (2 * pr * qr) / den)%R.

(* A basic condition over p and q *)
Definition cond_pqb (p q : Z) := p >= 0 /\ q > 0 /\ p <= q /\ (rel_prime p q).

(* Set of positive rational coordinates of the unit circle *)
Definition in_ucp_setb (x y : R) :=
  exists p : Z, exists q : Z,
  x = (fst (ucp p q)) /\ y = (snd (ucp p q)) /\ (cond_pqb p q).

Lemma rat_pos_coo1 : forall x y : R, (is_ucp (x,y)) ->
  exists r : R, (is_rat r) /\ (r >= 0)%R /\ (r <= 1)%R /\ x = (fst (p2 r)) /\
  y = (snd (p2 r)).
Proof.
  intros; unfold is_ucp in H; elim H; intros; elim H1; intros;
    elim (rat_coo2 x y (conj H0 H2)); intros; elim H4; intros.
(* Goal: @ex R (fun r : R => and (is_rat r) (and (Rge r (IZR Z0)) (and (Rle r (IZR (Zpos xH))) (and (@eq R x (@fst R R (p2 r))) (@eq R y (@snd R R (p2 r))))))) *)
  elim (interCDr_sol x0 x y).
  unfold eqp; simpl; intro; elim H7; intros; elim H3; simpl; intros;
    rewrite H8 in H10; elimtype False; generalize (Rge_le (-1) 0 H10)%R;
    fold (~ (0 <= -1)%R); apply Rlt_not_le; prove_sup.
  cut (0 < / (1 + x0 * x0))%R;
    [ intro
    | apply Rinv_0_lt_compat; rewrite <- (Rplus_0_r 0)%R;
      apply Rplus_lt_le_compat;
        [ prove_sup
        | fold (Rsqr x0); elim (Req_dec x0 0); intro;
          [ rewrite H7; rewrite Rsqr_0; unfold Rle; right; auto
          | unfold Rle; left; apply Rsqr_pos_lt; assumption ] ] ].
  unfold eqp; simpl; intro; elim H8; intros; elim H3; simpl; rewrite H9; 
(* Goal: and (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) (Rdiv (IZR a) (IZR b))) (Rplus (IZR (Zpos xH)) (Rmult (Rdiv (IZR a) (IZR b)) (Rdiv (IZR a) (IZR b))))) (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR a)) (IZR b)) (Rplus (Rmult (IZR a) (IZR a)) (Rmult (IZR b) (IZR b))))) (and (Z.ge a Z0) (and (Z.gt b Z0) (and (Z.le a b) (rel_prime a b)))) *)
    rewrite H10; intros; exists x0; split.
(* Goal: interCDr x0 x y *)
  assumption.
(* Goal: and (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) (Rdiv (IZR a) (IZR b))) (Rplus (IZR (Zpos xH)) (Rmult (Rdiv (IZR a) (IZR b)) (Rdiv (IZR a) (IZR b))))) (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR a)) (IZR b)) (Rplus (Rmult (IZR a) (IZR a)) (Rmult (IZR b) (IZR b))))) (and (Z.ge a Z0) (and (Z.gt b Z0) (and (Z.le a b) (rel_prime a b)))) *)
  split.
  generalize (Rge_le (2 * x0 / (1 + x0 * x0)) 0 H12); intro;
    rewrite Rmult_comm in H13;
    rewrite <- (Rmult_0_l (2 / (1 + x0 * x0))) in H13;
    cut (0 < 2 / (1 + x0 * x0))%R;
      [ intro; rewrite Rmult_comm in H13; unfold Rdiv in H13;
        rewrite (Rmult_assoc x0 2) in H13;
        rewrite (Rmult_comm x0 (2 * / (1 + x0 * x0)))%R in H13;
        generalize (Rmult_le_reg_l (2 / (1 + x0 * x0)) 0 x0 H14 H13); intro;
        apply Rle_ge; assumption
      | unfold Rdiv; prove_sup; assumption ].
(* Goal: and (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) (Rdiv (IZR a) (IZR b))) (Rplus (IZR (Zpos xH)) (Rmult (Rdiv (IZR a) (IZR b)) (Rdiv (IZR a) (IZR b))))) (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR a)) (IZR b)) (Rplus (Rmult (IZR a) (IZR a)) (Rmult (IZR b) (IZR b))))) (and (Z.ge a Z0) (and (Z.gt b Z0) (and (Z.le a b) (rel_prime a b)))) *)
  split.
  generalize (Rge_le ((1 - x0 * x0) / (1 + x0 * x0)) 0 H11); intro;
    unfold Rdiv in H13; rewrite Rmult_comm in H13;
    rewrite <- (Rmult_0_r (/ (1 + x0 * x0)))%R in H13;
    generalize (Rmult_le_reg_l (/ (1 + x0 * x0)) 0 (1 - x0 * x0) H7 H13)%R;
    intro; generalize (Rplus_le_compat_r (x0 * x0) 0 (1 - x0 * x0) H14)%R;
    intro; rewrite Rplus_0_l in H15; unfold Rminus in H15;
    rewrite Rplus_assoc in H15; rewrite Rplus_opp_l in H15;
    rewrite Rplus_0_r in H15; rewrite <- (Rmult_1_r 1) in H15;
    fold (Rsqr x0) in H15; fold (Rsqr 1) in H15;
    apply (Rsqr_incr_0_var x0 1 H15); unfold Rle; left; prove_sup.
(* Goal: and (@eq R (Rdiv (Rminus (IZR (Zpos xH)) (Rmult x0 x0)) (Rplus (IZR (Zpos xH)) (Rmult x0 x0))) (Rdiv (Rminus (IZR (Zpos xH)) (Rmult x0 x0)) (Rplus (IZR (Zpos xH)) (Rmult x0 x0)))) (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) x0) (Rplus (IZR (Zpos xH)) (Rmult x0 x0))) (Rdiv (Rmult (IZR (Zpos (xO xH))) x0) (Rplus (IZR (Zpos xH)) (Rmult x0 x0)))) *)
(* Goal: interCDr x0 x y *)
  auto.
(* Goal: interCDr x0 x y *)
  assumption.
Qed.

Lemma rat_pos_coo2 : forall x y : R, (is_ucp (x,y)) -> (in_ucp_setb x y).
Proof.
  intros; elim (rat_pos_coo1 x y H); simpl; intros; elim H0; intros; elim H2;
    intros; elim H4; intros; elim H6; intros; elim (relp_rat x0 H1 H3 H5);
    intro; elim x1; unfold frac; intros; elim H9; intros; elim H11; intros;
    elim H13; intros; elim H15; intros; unfold in_ucp_setb; simpl;
    unfold cond_pqb; exists a; exists b; rewrite H7; rewrite H8; rewrite H17.
(* Goal: and (@eq R (Rdiv (Rminus (IZR (Zpos xH)) (Rmult (Rdiv (IZR a) (IZR b)) (Rdiv (IZR a) (IZR b)))) (Rplus (IZR (Zpos xH)) (Rmult (Rdiv (IZR a) (IZR b)) (Rdiv (IZR a) (IZR b))))) (Rdiv (Rminus (Rmult (IZR b) (IZR b)) (Rmult (IZR a) (IZR a))) (Rplus (Rmult (IZR a) (IZR a)) (Rmult (IZR b) (IZR b))))) (and (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) (Rdiv (IZR a) (IZR b))) (Rplus (IZR (Zpos xH)) (Rmult (Rdiv (IZR a) (IZR b)) (Rdiv (IZR a) (IZR b))))) (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR a)) (IZR b)) (Rplus (Rmult (IZR a) (IZR a)) (Rmult (IZR b) (IZR b))))) (and (Z.ge a Z0) (and (Z.gt b Z0) (and (Z.le a b) (rel_prime a b))))) *)
  cut (b <> 0); auto with zarith; intro.
(* Goal: and (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) (Rdiv (IZR a) (IZR b))) (Rplus (IZR (Zpos xH)) (Rmult (Rdiv (IZR a) (IZR b)) (Rdiv (IZR a) (IZR b))))) (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR a)) (IZR b)) (Rplus (Rmult (IZR a) (IZR a)) (Rmult (IZR b) (IZR b))))) (and (Z.ge a Z0) (and (Z.gt b Z0) (and (Z.le a b) (rel_prime a b)))) *)
  split.
(* Goal: @eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) (Rdiv (IZR a) (IZR b))) (Rplus (IZR (Zpos xH)) (Rmult (Rdiv (IZR a) (IZR b)) (Rdiv (IZR a) (IZR b))))) (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR a)) (IZR b)) (Rplus (Rmult (IZR a) (IZR a)) (Rmult (IZR b) (IZR b)))) *)
(* Goal: and (Z.ge a Z0) (and (Z.gt b Z0) (and (Z.le a b) (rel_prime a b))) *)
  field; split; discrR; auto with zarith reals.
(* Goal: and (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) (Rdiv (IZR a) (IZR b))) (Rplus (IZR (Zpos xH)) (Rmult (Rdiv (IZR a) (IZR b)) (Rdiv (IZR a) (IZR b))))) (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR a)) (IZR b)) (Rplus (Rmult (IZR a) (IZR a)) (Rmult (IZR b) (IZR b))))) (and (Z.ge a Z0) (and (Z.gt b Z0) (and (Z.le a b) (rel_prime a b)))) *)
  split.
(* Goal: @eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) (Rdiv (IZR a) (IZR b))) (Rplus (IZR (Zpos xH)) (Rmult (Rdiv (IZR a) (IZR b)) (Rdiv (IZR a) (IZR b))))) (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR a)) (IZR b)) (Rplus (Rmult (IZR a) (IZR a)) (Rmult (IZR b) (IZR b)))) *)
(* Goal: and (Z.ge a Z0) (and (Z.gt b Z0) (and (Z.le a b) (rel_prime a b))) *)
  field; split; discrR; auto with zarith reals.
(* Goal: and (@eq R (Rdiv (Rminus (IZR (Zpos xH)) (Rmult x0 x0)) (Rplus (IZR (Zpos xH)) (Rmult x0 x0))) (Rdiv (Rminus (IZR (Zpos xH)) (Rmult x0 x0)) (Rplus (IZR (Zpos xH)) (Rmult x0 x0)))) (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) x0) (Rplus (IZR (Zpos xH)) (Rmult x0 x0))) (Rdiv (Rmult (IZR (Zpos (xO xH))) x0) (Rplus (IZR (Zpos xH)) (Rmult x0 x0)))) *)
(* Goal: interCDr x0 x y *)
  tauto.
Qed.

(* Step 5 *)

(* The full condition over p and q *)
Definition cond_pq (p q : Z) := cond_pqb p q /\ (distinct_parity p q).

(* The (new) set of positive rational coordinates of the unit circle *)
Definition in_ucp_set (x y : R) :=
  exists p : Z, exists q : Z,
  (x = (fst (ucp p q)) /\ y = (snd (ucp p q)) \/
   x = (snd (ucp p q)) /\ y = (fst (ucp p q))) /\ (cond_pq p q).

(* Inclusion of in_ucp_set in in_ucp_setb *)
Lemma nrat_pos_coo1 : forall x y : R, (in_ucp_set x y) -> (in_ucp_setb x y).
Proof.
(* Goal: forall (x y : R) (_ : in_ucp_set x y), in_ucp_setb x y *)
  unfold in_ucp_set, in_ucp_setb, cond_pq, cond_pqb; simpl; intros; elim_hyps.
(* Goal: @ex Z (fun p : Z => @ex Z (fun q : Z => and (or (and (@eq R x (Rdiv (Rminus (Rmult (IZR q) (IZR q)) (Rmult (IZR p) (IZR p))) (Rplus (Rmult (IZR p) (IZR p)) (Rmult (IZR q) (IZR q))))) (@eq R y (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR p)) (IZR q)) (Rplus (Rmult (IZR p) (IZR p)) (Rmult (IZR q) (IZR q)))))) (and (@eq R x (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR p)) (IZR q)) (Rplus (Rmult (IZR p) (IZR p)) (Rmult (IZR q) (IZR q))))) (@eq R y (Rdiv (Rminus (Rmult (IZR q) (IZR q)) (Rmult (IZR p) (IZR p))) (Rplus (Rmult (IZR p) (IZR p)) (Rmult (IZR q) (IZR q))))))) (and (and (Z.ge p Z0) (and (Z.gt q Z0) (and (Z.le p q) (rel_prime p q)))) (or (and (Zeven p) (Zodd q)) (and (Zodd p) (Zeven q)))))) *)
(* Goal: @ex Z (fun p : Z => @ex Z (fun q : Z => and (or (and (@eq R x (Rdiv (Rminus (Rmult (IZR q) (IZR q)) (Rmult (IZR p) (IZR p))) (Rplus (Rmult (IZR p) (IZR p)) (Rmult (IZR q) (IZR q))))) (@eq R y (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR p)) (IZR q)) (Rplus (Rmult (IZR p) (IZR p)) (Rmult (IZR q) (IZR q)))))) (and (@eq R x (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR p)) (IZR q)) (Rplus (Rmult (IZR p) (IZR p)) (Rmult (IZR q) (IZR q))))) (@eq R y (Rdiv (Rminus (Rmult (IZR q) (IZR q)) (Rmult (IZR p) (IZR p))) (Rplus (Rmult (IZR p) (IZR p)) (Rmult (IZR q) (IZR q))))))) (and (and (Z.ge p Z0) (and (Z.gt q Z0) (and (Z.le p q) (rel_prime p q)))) (or (and (Zeven p) (Zodd q)) (and (Zodd p) (Zeven q)))))) *)
  exists x0; exists x1; intuition.
  exists (x1 - x0); exists (x0 + x1); rewrite plus_IZR; rewrite <- Z_R_minus;
    rewrite H; rewrite H5.
  replace
   ((IZR x1 - IZR x0) * (IZR x1 - IZR x0) +
    (IZR x0 + IZR x1) * (IZR x0 + IZR x1))%R with
(* Goal: @eq R (Rminus (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (Rmult (Rmult (IZR (Zpos (xO (xO xH)))) (Rplus (IZR (Zpos xH)) (Rmult r r))) (Rminus (Rmult r r) (IZR (Zpos xH))))) (IZR (Zpos (xO (xO xH)))) *)
(* Goal: Delta_is_pos (mknonzeroreal (Rplus (IZR (Zpos xH)) (Rmult r r)) H3) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rminus (Rmult r r) (IZR (Zpos xH))) *)
(* Goal: not (@eq R (Rplus (IZR (Zpos xH)) (Rmult r r)) (IZR Z0)) *)
(* Goal: @eq R (Rplus (Rplus (Rmult (Rplus (IZR (Zpos xH)) (Rmult r r)) (Rsqr x)) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) x)) (Rminus (Rmult r r) (IZR (Zpos xH)))) (IZR Z0) *)
   (2 * (IZR x0 * IZR x0 + IZR x1 * IZR x1))%R by  ring.
(* Goal: and (@eq R (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR x0)) (IZR x1)) (Rplus (Rmult (IZR x0) (IZR x0)) (Rmult (IZR x1) (IZR x1)))) (Rdiv (Rminus (Rmult (Rplus (IZR x0) (IZR x1)) (Rplus (IZR x0) (IZR x1))) (Rmult (Rminus (IZR x1) (IZR x0)) (Rminus (IZR x1) (IZR x0)))) (Rmult (IZR (Zpos (xO xH))) (Rplus (Rmult (IZR x0) (IZR x0)) (Rmult (IZR x1) (IZR x1)))))) (and (@eq R (Rdiv (Rminus (Rmult (IZR x1) (IZR x1)) (Rmult (IZR x0) (IZR x0))) (Rplus (Rmult (IZR x0) (IZR x0)) (Rmult (IZR x1) (IZR x1)))) (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (Rminus (IZR x1) (IZR x0))) (Rplus (IZR x0) (IZR x1))) (Rmult (IZR (Zpos (xO xH))) (Rplus (Rmult (IZR x0) (IZR x0)) (Rmult (IZR x1) (IZR x1)))))) (and (Z.ge (Z.sub x1 x0) Z0) (and (Z.gt (Z.add x0 x1) Z0) (and (Z.le (Z.sub x1 x0) (Z.add x0 x1)) (rel_prime (Z.sub x1 x0) (Z.add x0 x1)))))) *)
  split;[idtac|split]; try (field; neq_0;apply sqr_sum; auto with zarith).
(* Goal: not (@eq Z (Z.add (Z.mul a a) (Z.mul b b)) Z0) *)
(* Goal: @eq R (Rdiv (Rminus (IZR (Zpos xH)) (Rmult x0 x0)) (Rplus (IZR (Zpos xH)) (Rmult x0 x0))) (Rdiv (IZR (Z.sub (Z.mul b b) (Z.mul a a))) (IZR (Z.add (Z.mul a a) (Z.mul b b)))) *)
(* Goal: @ex (prod Z Z) (fun pq : prod Z Z => let (p, q) := pq in and (not (@eq Z q Z0)) (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) x0) (Rplus (IZR (Zpos xH)) (Rmult x0 x0))) (Rdiv (IZR p) (IZR q)))) *)
  do 3 try split; auto with zarith.
(* Goal: not (@eq Z (Z.add (Z.mul a a) (Z.mul b b)) Z0) *)
(* Goal: @eq R (Rdiv (Rminus (IZR (Zpos xH)) (Rmult x0 x0)) (Rplus (IZR (Zpos xH)) (Rmult x0 x0))) (Rdiv (IZR (Z.sub (Z.mul b b) (Z.mul a a))) (IZR (Z.add (Z.mul a a) (Z.mul b b)))) *)
(* Goal: @ex (prod Z Z) (fun pq : prod Z Z => let (p, q) := pq in and (not (@eq Z q Z0)) (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) x0) (Rplus (IZR (Zpos xH)) (Rmult x0 x0))) (Rdiv (IZR p) (IZR q)))) *)
  generalize (prop1 _ _ H4 H1); auto with zarith.
Qed.

(* Inclusion of in_ucp_setb in in_ucp_set *)
Lemma nrat_pos_coo2 : forall x y : R, (in_ucp_setb x y) -> (in_ucp_set x y).
Proof.
  unfold in_ucp_setb, in_ucp_set, cond_pq, cond_pqb, distinct_parity; simpl;
    intros; elim_hyps.
(* Goal: @ex Z (fun p : Z => @ex Z (fun q : Z => and (or (and (@eq R x (Rdiv (Rminus (Rmult (IZR q) (IZR q)) (Rmult (IZR p) (IZR p))) (Rplus (Rmult (IZR p) (IZR p)) (Rmult (IZR q) (IZR q))))) (@eq R y (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR p)) (IZR q)) (Rplus (Rmult (IZR p) (IZR p)) (Rmult (IZR q) (IZR q)))))) (and (@eq R x (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR p)) (IZR q)) (Rplus (Rmult (IZR p) (IZR p)) (Rmult (IZR q) (IZR q))))) (@eq R y (Rdiv (Rminus (Rmult (IZR q) (IZR q)) (Rmult (IZR p) (IZR p))) (Rplus (Rmult (IZR p) (IZR p)) (Rmult (IZR q) (IZR q))))))) (and (and (Z.ge p Z0) (and (Z.gt q Z0) (and (Z.le p q) (rel_prime p q)))) (or (and (Zeven p) (Zodd q)) (and (Zodd p) (Zeven q)))))) *)
  elim (relp_parity x0 x1 H4); intro.
(* Goal: @ex Z (fun p : Z => @ex Z (fun q : Z => and (or (and (@eq R x (Rdiv (Rminus (Rmult (IZR q) (IZR q)) (Rmult (IZR p) (IZR p))) (Rplus (Rmult (IZR p) (IZR p)) (Rmult (IZR q) (IZR q))))) (@eq R y (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR p)) (IZR q)) (Rplus (Rmult (IZR p) (IZR p)) (Rmult (IZR q) (IZR q)))))) (and (@eq R x (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR p)) (IZR q)) (Rplus (Rmult (IZR p) (IZR p)) (Rmult (IZR q) (IZR q))))) (@eq R y (Rdiv (Rminus (Rmult (IZR q) (IZR q)) (Rmult (IZR p) (IZR p))) (Rplus (Rmult (IZR p) (IZR p)) (Rmult (IZR q) (IZR q))))))) (and (and (Z.ge p Z0) (and (Z.gt q Z0) (and (Z.le p q) (rel_prime p q)))) (or (and (Zeven p) (Zodd q)) (and (Zodd p) (Zeven q)))))) *)
(* Goal: @ex Z (fun p : Z => @ex Z (fun q : Z => and (or (and (@eq R x (Rdiv (Rminus (Rmult (IZR q) (IZR q)) (Rmult (IZR p) (IZR p))) (Rplus (Rmult (IZR p) (IZR p)) (Rmult (IZR q) (IZR q))))) (@eq R y (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR p)) (IZR q)) (Rplus (Rmult (IZR p) (IZR p)) (Rmult (IZR q) (IZR q)))))) (and (@eq R x (Rdiv (Rmult (Rmult (IZR (Zpos (xO xH))) (IZR p)) (IZR q)) (Rplus (Rmult (IZR p) (IZR p)) (Rmult (IZR q) (IZR q))))) (@eq R y (Rdiv (Rminus (Rmult (IZR q) (IZR q)) (Rmult (IZR p) (IZR p))) (Rplus (Rmult (IZR p) (IZR p)) (Rmult (IZR q) (IZR q))))))) (and (and (Z.ge p Z0) (and (Z.gt q Z0) (and (Z.le p q) (rel_prime p q)))) (or (and (Zeven p) (Zodd q)) (and (Zodd p) (Zeven q)))))) *)
  exists x0; exists x1; intuition.
  unfold both_odd in H5; elim_hyps; generalize (Zodd_def1 _ H5); clear H5;
    intro; generalize (Zodd_def1 _ H6); clear H6; intro; elim_hyps.
  exists (x2 - x3); exists (x2 + x3 + 1); split;
    [ right; rewrite H; rewrite H0; rewrite H5; rewrite H6; atomic_IZR; simpl;
      split; field; split; neq_0; apply sqr_sum; auto with zarith
    | rewrite H5 in H1; rewrite H6 in H2; rewrite H5 in H3; rewrite H6 in H3;
      do 4 try split; auto with zarith ].
  apply rel_prime_sym; apply relp_sum; ring_simplify (x2 + x3 + 1 + (x2 - x3));
    ring_simplify (x2 + x3 + 1 - (x2 - x3)); generalize H5; clear H5;
    ring_simplify (2 * x3 + 1);
    intro; generalize H6; clear H6; ring_simplify (2 * x2 + 1); intro;
(* Goal: not (@eq Z (Z.add (Z.mul a a) (Z.mul b b)) Z0) *)
(* Goal: @eq R (Rdiv (Rminus (IZR (Zpos xH)) (Rmult x0 x0)) (Rplus (IZR (Zpos xH)) (Rmult x0 x0))) (Rdiv (IZR (Z.sub (Z.mul b b) (Z.mul a a))) (IZR (Z.add (Z.mul a a) (Z.mul b b)))) *)
(* Goal: @ex (prod Z Z) (fun pq : prod Z Z => let (p, q) := pq in and (not (@eq Z q Z0)) (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) x0) (Rplus (IZR (Zpos xH)) (Rmult x0 x0))) (Rdiv (IZR p) (IZR q)))) *)
    rewrite <- H5; rewrite <- H6; auto with zarith.
  elim (Zeven_odd_dec x2); intro; elim (Zeven_odd_dec x3); intro; Zparity_hyps;
    rewrite H7; rewrite H8;
    [ left; split; [ apply Zeven_def2; exists (x4 - x5)
                   | apply Zodd_def2; exists (x4 + x5) ]
    | right; split; [ apply Zodd_def2; exists (x5 - x4 - 1)
                    | apply Zeven_def2; exists (x5 + x4 + 1) ]
    | right; split; [ apply Zodd_def2; exists (x4 - x5)
                    | apply Zeven_def2; exists (x4 + x5 + 1) ]
    | left; split; [ apply Zeven_def2; exists (x4 - x5)
(* Goal: @eq R (Rminus (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r)) (Rmult (Rmult (IZR (Zpos (xO (xO xH)))) (Rplus (IZR (Zpos xH)) (Rmult r r))) (Rminus (Rmult r r) (IZR (Zpos xH))))) (IZR (Zpos (xO (xO xH)))) *)
(* Goal: Delta_is_pos (mknonzeroreal (Rplus (IZR (Zpos xH)) (Rmult r r)) H3) (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) (Rminus (Rmult r r) (IZR (Zpos xH))) *)
(* Goal: not (@eq R (Rplus (IZR (Zpos xH)) (Rmult r r)) (IZR Z0)) *)
(* Goal: @eq R (Rplus (Rplus (Rmult (Rplus (IZR (Zpos xH)) (Rmult r r)) (Rsqr x)) (Rmult (Rmult (Rmult (IZR (Zpos (xO xH))) r) r) x)) (Rminus (Rmult r r) (IZR (Zpos xH)))) (IZR Z0) *)
                   | apply Zodd_def2; exists (x4 + x5 + 1) ] ]; ring.
Qed.

(* step 6 *)

(* The set of Pythagorean triples *)
Definition pytha_set (a b c : Z) :=
  exists p : Z, exists q : Z, exists m : Z,
    (a = m * (q * q - p * p) /\ b = 2 * m * (p * q) \/
     a = 2 * m * (p * q) /\ b = m * (q * q - p * p)) /\
    c = m * (p * p + q * q) /\ m >= 0 /\ (cond_pq p q).

(* Relative primality and fractions *)
Lemma relp_frac : forall a b c d : Z,
  (b <> 0) -> (d <> 0) -> (frac a b) = (frac c d) -> (rel_prime c d) ->
  exists m : Z, m <> 0 /\ b = m * d.
Proof.
(* Goal: forall (a b c d : Z) (_ : not (@eq Z b Z0)) (_ : not (@eq Z d Z0)) (_ : @eq R (frac a b) (frac c d)) (_ : rel_prime c d), @ex Z (fun m : Z => and (not (@eq Z m Z0)) (@eq Z b (Z.mul m d))) *)
  unfold frac; intros.
(* Goal: @ex Z (fun m : Z => and (not (@eq Z m Z0)) (@eq Z b (Z.mul m d))) *)
  cut (c * b = a * d).
  intro; cut (d | c * b);
    [ intro; cut (rel_prime d c);
        try (intro; generalize (Gauss d c b H4 H5); intro; destruct H6 as (q,H6);
        exists q; intuition; rewrite H7 in H6); auto with zarith
    | apply (Zdivide_intro _ _ a H3) ].
  generalize (Rmult_eq_compat_l (IZR b * IZR d) _ _ H1); clear H1; intro;
    replace (IZR b * IZR d * (IZR a / IZR b))%R
            with ((IZR a) * (IZR d))%R in H1;
      [ replace (IZR b * IZR d * (IZR c / IZR d))%R
                with ((IZR c) * (IZR b))%R in H1;
        [ repeat rewrite <- mult_IZR in H1; generalize (eq_IZR _ _ H1); auto
        | field; discrR; assumption ]
      | field; discrR; assumption ].
Qed.

Lemma pytha_thm1 : forall a b c : Z, (is_pytha a b c) -> (pytha_set a b c).
Proof.
  do 3 intro; elim (Z_gt_dec c 0); [ idtac
    | unfold is_pytha, pytha_set, pos_triple, cond_pq, cond_pqb ]; intros.
  generalize (pytha_ucirc1 _ _ _ a0 H); intro;
    cut (is_ucp (frac a c, frac b c));
      [ clear H0; intro; generalize (rat_pos_coo2 _ _ H0); clear H0; intro;
        generalize (nrat_pos_coo2 _ _ H0); clear H0; intro;
        unfold in_ucp_set, cond_pq, cond_pqb in H0;
        unfold pytha_set, cond_pq, cond_pqb; simpl in H0; elim_hyps;
        generalize (relp_pq1 _ _ H1 H4 H5 H2); intro;
        generalize (Zgt_lt _ _ a0); intro; generalize (Zlt_not_eq _ _ H8);
        clear H8; intro; generalize (sym_not_eq H8); clear H8; intro;
        generalize (Zgt_lt _ _ H3); intro; generalize (Zlt_not_eq _ _ H9);
        clear H9; intro; generalize (sym_not_eq H9); clear H9; intro;
        (cut (x * x + x0 * x0 <> 0); [ intro | auto with zarith ];
        (cut ((IZR x0 * IZR x0 - IZR x * IZR x) /
             (IZR x * IZR x + IZR x0 * IZR x0) =
             frac (x0 * x0 - x * x) (x * x + x0 * x0))%R;
          [ intro | head_IZR; auto ];
        (cut (2 * IZR x * IZR x0 / (IZR x * IZR x + IZR x0 * IZR x0) =
             frac (2 * x * x0) (x * x + x0 * x0))%R;
          [ intro | head_IZR; auto ])))
      | idtac ].
  rewrite H11 in H0; clear H11; rewrite H12 in H6; clear H12;
    generalize (relp_frac _ _ _ _ H8 H10 H0 H7); intro; elim_hyps;
    rewrite H12 in H0; rewrite H12 in H6; exists x; exists x0; exists x1;
    generalize (frac_eq _ _ _ _ H11 H10 H0); clear H0; intro;
    generalize (frac_eq _ _ _ _ H11 H10 H6); clear H6; intro;
    rewrite H0; rewrite H6; rewrite H12; intuition; (left; split; ring) ||
    (cut (x1 * (x * x + x0 * x0) > 0);
      [ intro; rewrite Zmult_comm in H13; cut (x * x + x0 * x0 > 0);
        try (intro; generalize (Zmult_gt_0_reg_l _ _ H14 H13));
        auto with zarith
      | rewrite <- H12; assumption ]).
  rewrite H11 in H6; clear H11; rewrite H12 in H0; clear H12;
    generalize (relp_frac _ _ _ _ H8 H10 H6 H7); intro; elim_hyps;
    rewrite H12 in H0; rewrite H12 in H6; exists x; exists x0; exists x1;
    generalize (frac_eq _ _ _ _ H11 H10 H0); clear H0; intro;
    generalize (frac_eq _ _ _ _ H11 H10 H6); clear H6; intro;
    rewrite H0; rewrite H6; rewrite H12; intuition; (right; split; ring) ||
    (cut (x1 * (x * x + x0 * x0) > 0);
      [ intro; rewrite Zmult_comm in H13; cut (x * x + x0 * x0 > 0);
        try (intro; generalize (Zmult_gt_0_reg_l _ _ H14 H13)); 
        auto with zarith
      | rewrite <- H12; assumption ]).
  unfold is_ucp, is_ratp, is_posp; simpl; intuition; unfold is_rat;
    unfold is_pytha, pos_triple in H; elim_hyps; generalize (Zgt_lt _ _ a0);
    intro; generalize (IZR_lt _ _ H4); intro; simpl in H5;
    fold (IZR c > 0)%R in H5;
    [ exists (a, c); intuition | exists (b, c); intuition
    | unfold frac; generalize (IZR_ge _ _ H); clear H; intro; simpl in H
    | unfold frac; generalize (IZR_ge _ _ H2); clear H2; intro; simpl in H2 ];
    auto with reals.
  elim_hyps; cut (c = 0);
    [ intro; exists 0; exists 1; exists 0; rewrite H3; simpl; intuition;
      (left; rewrite H3 in H0; simpl in H0; progress auto with zarith)
      || (compute; auto with zarith)
    | auto with zarith ].
Qed.

Lemma pytha_thm2 : forall a b c : Z, (pytha_set a b c) -> (is_pytha a b c).
Proof.
  unfold pytha_set, is_pytha, cond_pq, cond_pqb, pos_triple; intros; elim_hyps;
    rewrite H; rewrite H7; rewrite H0; split; ring || (intuition; apply Zle_ge;
    generalize (Zge_le _ _ H2); clear H2; intro; generalize (Zgt_lt _ _ H4);
    clear H4; intro; generalize (Zlt_le_weak _ _ H4); intro;
    repeat apply Zmult_le_0_compat; auto with zarith).
Qed.

(* A specific case *)

Definition pytha_set_even (a b c : Z) :=
  exists p : Z, exists q : Z, exists m : Z,
    a = m * (q * q - p * p) /\ b = 2 * m * (p * q) /\
    c = m * (p * p + q * q) /\ m >= 0 /\ (cond_pq p q).

Lemma pytha_thm3 : forall a b c : Z,
  is_pytha a b c -> Zodd a -> pytha_set_even a b c.
Proof.
  intros; elim (pytha_thm1 _ _ _ H); clear H; intros;
    unfold cond_pq, cond_pqb in H; elim_hyps;
    unfold pytha_set_even, cond_pq, cond_pqb; exists x; exists x0; exists x1;
    try solve [ intuition ].
  elimtype False; rewrite <- Zmult_assoc in H;
  generalize (Zeven_def2 _ (ex_intro (fun x => a = 2 * x) (x1 * (x * x0)) H));
(* Goal: and (@eq R (Rdiv (Rminus (IZR (Zpos xH)) (Rmult x0 x0)) (Rplus (IZR (Zpos xH)) (Rmult x0 x0))) (Rdiv (Rminus (IZR (Zpos xH)) (Rmult x0 x0)) (Rplus (IZR (Zpos xH)) (Rmult x0 x0)))) (@eq R (Rdiv (Rmult (IZR (Zpos (xO xH))) x0) (Rplus (IZR (Zpos xH)) (Rmult x0 x0))) (Rdiv (Rmult (IZR (Zpos (xO xH))) x0) (Rplus (IZR (Zpos xH)) (Rmult x0 x0)))) *)
(* Goal: interCDr x0 x y *)
  intro; generalize (Zeven_not_Zodd _ H9); auto.
Qed.
