Require Import BinPos.
Open Scope positive_scope.

Ltac mysimpl := simplify_eq; repeat rewrite Pmult_xO_permute_r. 

Theorem main_thm: forall p q: positive, 2*(q*q)<>p*p.
Proof.
induction p; simpl; intro; mysimpl.
destruct q; mysimpl; firstorder.
Qed.

Require Import Reals Field.
Open Scope R_scope.

(* IPR: Injection from Positive to Reals *)
(* Should be in the standard library, close to INR and IZR *)

Definition IPR (p:positive):= (INR (nat_of_P p)).
Coercion IPR : positive >-> R.

Lemma mult_IPR : forall p q, IPR (p * q) = (IPR p * IPR q)%R.
unfold IPR; intros; rewrite nat_of_P_mult_morphism; auto with real.
Qed.
Lemma IPR_eq : forall p q, IPR p = IPR q -> p = q.
unfold IPR; intros; apply nat_of_P_inj; auto with real.
Qed.
Lemma IPR_nonzero : forall p, IPR p <> 0.
unfold IPR; auto with real.
Qed.
Hint Resolve IPR_eq IPR_nonzero.
(* End of IPR *)

Ltac myfield := field; rewrite <- mult_IPR; auto.

Lemma main_thm_pos_rat : forall (p q:positive), 2 <> (p/q)*(p/q).
Proof.
red; intros.
assert (2*(q*q)=p*p).
  rewrite H; myfield.
clear H; change 2 with (IPR 2) in H0.
apply main_thm with p q; auto.
repeat rewrite <- mult_IPR in H0; auto.
Qed.

Coercion IZR : Z >-> R.

Lemma main_thm_rat : forall (p:Z)(q:positive), 2 <> (p/q)*(p/q).
Proof.
destruct p; simpl; intros.
replace (0 / q * (0 / q)) with 0.
discrR.
field; rewrite <- mult_IPR; auto.
exact (main_thm_pos_rat p q).
replace (INR (nat_of_P p)) with (IPR p); auto.
replace (- p / q * (- p / q)) with ((p/q)*(p/q)); try myfield.
exact (main_thm_pos_rat p q).
Qed.

Definition irrational (x:R) : Prop := forall (p:Z)(q:positive), x <> (p/q).

Lemma Sqrt2_irr : irrational (sqrt 2).
Proof.
 red; intros p q H.
 assert (H1: 2 = sqrt 2 * sqrt 2).
   symmetry; apply sqrt_sqrt; auto with real.
 rewrite H in H1; apply main_thm_rat with p q; auto.
Qed.