proposition: Theorem thm_irrational : forall (p q : nat), q <> 0 -> sqrt 2 <> (INR p / INR q)%R.
proof: Proof. unfold not. intros p q H H0. assert (2 * q * q = p * p). { assert (((sqrt 2) ^ 2)%R = 2%R). { hauto use: @Rsqr_sqrt, @Rlt_R0_R2, @Rsqr_pow2 unfold: Rle. } assert (((INR p / INR q) ^ 2)%R = ((INR p / INR q) * (INR p / INR q))%R). { qauto use: @Rsqr_pow2 unfold: Rsqr. } assert (((INR p / INR q) * (INR p / INR q))%R = ((INR p * INR p) / (INR q * INR q))%R). { hauto use: @Rsqr_div, @not_0_INR. } assert (HH: 2%R = ((INR p * INR p) / (INR q * INR q))%R) by sauto. assert (INR q <> 0%R). { qauto use: @INR_not_0, @INR_eq. } assert (HH2: (2 * INR q * INR q)%R = (INR p * INR p)%R). { rewrite HH; rewrite Rmult_assoc. hfcrush use: @Rinv_l_sym, @Rmult_1_r, @Rmult_integral_contrapositive_currified, @Rmult_assoc unfold: Rsqr, Rdiv. } clear -HH2. assert (forall a b, INR a = INR b -> a = b). { qauto use: @INR_eq. } assert (INR (2 * q * q) = INR (p * p)). { assert (INR (p * p) = (INR p * INR p)%R). { hfcrush use: @mult_INR. } assert (INR (2 * q * q) = (2 * INR q * INR q)%R). { assert (INR (2 * q * q) = (INR 2 * INR q * INR q)%R). { hauto ered: off use: @mult_INR. } sauto. } sauto. } sauto. } sauto use: lem_main. Qed.
imports: Hammer(Tactics) Reals Arith Wf_nat Even Lia