(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

set "baseuri" "cic:/matita/Z/prova".

include "nat/factorization.ma".

lemma divides_p_times_n_n_to_divides_p_n:
\forall n:nat.\forall p:nat. prime p \to p \divides n*n \to p \divides n.
intros.
elim (divides_times_to_divides ? ? ? ? H1);assumption.
qed.

lemma not_eq_S: \forall n,m:nat. S(S O)*n\neq S (S(S O)*m).
apply nat_elim2
  [intro.simplify.apply not_eq_O_S
  |intro.simplify.unfold.intro.apply (not_eq_O_S (n+n)).symmetry.
   rewrite > plus_n_Sm.
   rewrite > plus_n_O in \vdash (? ? (? ? %) ?).
   apply inj_S.assumption
  |intros.
  rewrite > sym_times.
  rewrite > sym_times in \vdash (? (? ? ? (? %))).
  simplify.
  rewrite > sym_times.
  rewrite > sym_times in \vdash (? (? ? ? (? (? (? %))))).
  unfold. intro.
  apply H.apply inj_S.apply inj_S.assumption
  ]
qed.

(* p_ord n p gives the power of p in n and the "remainder" m.
   That is, if p_ord n p = <q,r> then n=r*p^q and p does not divide r.
   p_ord is used in factorization.ma for the factorization of natural
   numbers. 
   Suppose that 
      p_ord n p = <q1,r1> and
      p_ord m p = <q2,r2>       
   Then p_ord (n*m) p = p_ord m p = <q1+q2,r1*r2>. 
   In particular, if n*n = p*m*m, then
   
   2*q1 = q1+q1 = fst (p_ord n*n p) = fst (p_ord p*m*m p) = 1+q2+q2 = 1+2*q2

   that is absurd by not_eq_S above.
 *)
 
theorem main: \forall n,m:nat.\forall p:nat. O \lt n \to 
O \lt m \to prime p \to n * n \neq p * (m * m).
intros.
cut (S O \lt p)
  [cut (O \lt p)
    [cut (O \lt m*m)
      [unfold. intro.
       apply (not_eq_S (fst ? ? (p_ord n p)) (fst ? ? (p_ord m p))).
       rewrite > plus_n_O in \vdash (? ? ? (? %)).
       rewrite > plus_n_Sm.
       rewrite < times_SSO_n. 
       rewrite < times_SSO_n.
       rewrite < (fst_p_ord_times ? ? ? H2 H H).
       rewrite < (fst_p_ord_times ? ? ? H2 H1 H1).
       rewrite > H3.
       rewrite > (fst_p_ord_times ? ? ? H2 Hcut1 Hcut2).
       rewrite > sym_plus.
       rewrite > (p_ord_p p Hcut).
       reflexivity.
      |rewrite > (times_n_O O).
       apply lt_times [apply H1|apply H1]
      ]
    |apply (trans_lt ? (S O)) [unfold.apply le_n|assumption]
    ]
  |unfold prime in H2.elim H2.assumption
  ]
qed.