Theory Periodicity_Lemma

(*  Title:      CoW/Periodicity_Lemma.thy
    Author:     Štěpán Holub, Charles University

Part of Combinatorics on Words Formalized. See https://gitlab.com/formalcow/combinatorics-on-words-formalized/
*)

theory Periodicity_Lemma
  imports CoWBasic
begin

chapter "The Periodicity Lemma"

text‹The Periodicity Lemma says that if a sufficiently long word has two periods p and q,
then the period can be refined to @{term "gcd p q"}.
The consequence is equivalent to the fact that the corresponding periodic roots commute.
``Sufficiently long'' here means at least @{term "p + q - gcd p q"}.
It is also known as the Fine and Wilf theorem due to its authors @{cite FineWilf}.›

text‹
If we relax the requirement to @{term "p + q"}, then the claim becomes easy, and it is proved in @{theory Combinatorics_Words.CoWBasic} as @{term two_pers_root}: @{thm[names_long] two_pers_root[no_vars]}.
›

theorem per_lemma_relaxed:
  assumes "period w p" and  "period w q" and  "p + q  |w|"
  shows "(take p w)(take q w) = (take q w)(take p w)"
  using   two_pers_root[OF
      period w p[unfolded period_def[of w p]]
      period w q[unfolded period_def[of w q]], unfolded
      take_len[OF add_leD1[OF p + q  |w|]]
      take_len[OF add_leD2[OF p + q  |w|]], OF p + q  |w|].

text‹Also in terms of the numeric period:›

thm two_periods

section ‹Main claim›

text‹We first formulate the claim of the Periodicity lemma in terms of commutation of two periodic roots.
For trivial reasons we can also drop the requirement that the roots are nonempty.
›

theorem per_lemma_comm:
  assumes "w ≤p r  w" and "w ≤p s  w"
    and len: "|r| + |s| - (gcd |r| |s|)  |w|"
  shows "r  s = s  r"
  using assms
proof (induction "|s| + |s| + |r|" arbitrary: w r s rule: less_induct)
  case less
  consider (empty) "s = ε" | (short)  "|r| < |s|" | (step) "s  ε  |s|  |r|" by force
  then show ?case
  proof (cases)
    case (empty)
    thus "r  s = s  r" by fastforce
  next
    case (short)
    thus "r  s = s  r"
      using  "less.hyps"[OF  _ w ≤p s  w w ≤p r  w
      |r| + |s| - (gcd |r| |s|)  |w|[unfolded gcd.commute[of "|r|"] add.commute[of "|r|"]]] by fastforce
   next
     case (step)
    hence  "s  ε" and "|s|  |r|" by blast+
    from le_add_diff[OF gcd_le2_nat[OF s  ε[folded length_0_conv], of "|r|"], unfolded gcd.commute[of "|r|"], of "|r|"]
    have "|r|  |w|"
      using  |r| + |s| - (gcd |r| |s|)  |w|[unfolded gcd.commute[of "|r|"] add.commute[of "|r|"]] order.trans by blast
    hence "|s|  |w|"
      using |s|  |r| order.trans by blast
    from pref_prod_long[OF  w ≤p s  w this]
    have "s ≤p w".

    obtain w' where "s  w' = w" and "|w'| < |w|"
      using s  ε s ≤p w[unfolded prefix_def]
      by force
    have "w' ≤p w"
      using w ≤p s  w unfolding s  w' = w[symmetric] pref_cancel_conv.
    from this[folded s  w' = w]
    have "w' ≤p sw'".

    have "s ≤p r"
      using pref_prod_le[OF prefix_order.trans[OF s ≤p w w ≤p r  w] |s|  |r|].
    hence  "w' ≤p (s¯>r)  w'"
      using w ≤p r  w s  w' = w pref_prod_pref[OF _ w' ≤p w, of "s¯>r"]
      unfolding prefix_def by fastforce

   have ind_len: "|s¯>r| + |s|  - (gcd |s¯>r| |s|)  |w'|"
      using |r| + |s| - (gcd |r| |s|)  |w|[folded s  w' = w]
      unfolding pref_gcd_lq[OF s ≤p r, unfolded gcd.commute[of "|s|"]] lenmorph lq_short_len[OF s ≤p r, unfolded add.commute[of "|s|"]] by force

    have "s  s¯>r = s¯>r  s"
      using "less.hyps"[OF  _ w' ≤p (s¯>r)  w'  w' ≤p s  w' ind_len] s ≤p r |w'| < |w|
        unfolding prefix_def
        by force

    thus "r  s = s  r"
       using s ≤p r by (fastforce simp add: prefix_def)
  qed
qed

lemma per_lemma_comm_pref:
  assumes "u ≤p r@k" "u ≤p s@l"
      and len: "|r| + |s| - gcd (|r|) (|s|)  |u|"
    shows "r  s = s  r"
  using  pref_prod_root[OF assms(2)] pref_prod_root[OF assms(1)] per_lemma_comm[OF _ _ len] by blast

text‹We can now prove the numeric version.›

theorem per_lemma: assumes "period w p" and "period w q" and len: "p + q - gcd p q  |w|"
  shows  "period w (gcd p q)"
proof-
  have takep: "w ≤p (take p w)  w" and takeq: "w ≤p (take q w)  w"
    using period w p period w q per_pref by blast+
  have "p  |w|"
    using per_lemma_len_le[OF len] per_not_zero[OF period w q].
  have lenp: "|take p w| = p"
    using gcd_le2_pos[OF per_not_zero[OF period w q], of p] len take_len
    by auto
  have lenq: "|take q w| = q"
    using gcd_le1_pos[OF per_not_zero[OF period w p], of q] len take_len
    by simp
  obtain t where "take p w  t*" and "take q w  t*"
    using comm_rootE[OF per_lemma_comm[OF takep takeq, unfolded lenp lenq, OF len], of thesis] by blast
  have "w <p t  w"
    using period w p[unfolded period_def, THEN per_root_trans, OF take p w  t*].
  with per_nemp[OF period w q]
  have "period w |t|"
    by (rule periodI)
  have "|t| dvd (gcd p q)"
    using  common_root_len_gcd[OF take p w  t* take q w  t*] unfolding  lenp lenq.
  from dvd_div_mult_self[OF this]
  have "gcd p q div |t| * |t| = gcd p q".
  have "gcd p q  0"
    using period w p by auto
  from this[folded dvd_div_eq_0_iff[OF |t| dvd (gcd p q)]]
  show "period w (gcd p q)"
    using  per_mult[OF period w |t|, of "gcd p q div |t|", unfolded dvd_div_mult_self[OF |t| dvd (gcd p q)]] by blast
qed

section ‹Optimality›

text@{term "FW_word"} (where FW stands for  Fine and Wilf) yields a word which show the optimality of the bound in the Periodicity lemma.
    Moreover, the obtained word has maximum possible letters (each equality of letters is forced by periods). The latter is not proved here.›

term "butlast ([0..<(gcd p q)]@(p div (gcd p q)))[gcd p q](butlast ([0..<(gcd p q)]@(p div (gcd p q))))"

― ‹an auxiliary claim›
lemma ext_per_sum: assumes "period w p" and "period w q" and  "p  |w|"
  shows "period ((take p w)  w) (p+q)"
proof-
  have nemp: "take p w  take q w  ε"
    using period w p by auto
  have "take (p + q) (take p w  w) = take p (take p w  w)  take q (drop p (take p w  w))"
    using take_add by blast
  also have "... = take p w  take q w"
    by (simp add: p  |w|)
  ultimately have sum: "take (p + q) (take p w  w) = take p w  take q w"
    by presburger
  note assms[unfolded period_def]
  show ?thesis
    unfolding period_def sum rassoc
    using pref_spref_prolong[OF self_pref spref_spref_prolong[OF w <p take q w  w w <p take p w  w]].
qed

definition "fw_p_per p q  butlast ([0..<(gcd p q)]@(p div (gcd p q)))"
definition "fw_base p q  fw_p_per p q  [gcd p q] fw_p_per p q"

fun FW_word :: "nat  nat  nat list" where
  FW_word_def: "FW_word p q =
―‹symmetry›           (if q < p then  FW_word q p else
―‹artificial value›   if p = 0 then ε else
―‹artificial value›   if p = q then ε else
―‹base case›          if gcd p q = q - p then fw_base p q
―‹step›               else (take p (FW_word p (q-p)))  FW_word p (q-p))"

lemma FW_sym: "FW_word p q = FW_word q p"
  by (cases rule: linorder_cases[of p q]) simp+

theorem fw_word': "¬ p dvd q  ¬ q dvd p 
 |FW_word p q| = p + q - gcd p q - 1  period (FW_word p q) p  period (FW_word p q) q  ¬ period (FW_word p q) (gcd p q)"
proof (induction "p + p + q" arbitrary: p q rule: less_induct)
  case less
  have "p  0"
    using  ¬ q dvd p dvd_0_right[of q] by meson
  have "p  q"
    using ¬ p dvd q by auto
  then consider "q < p" | "p < q"
    by linarith
  then show ?case
  proof (cases)
    assume "q < p"
    have less: "q + q + p < p + p + q"
      by (simp add: q < p)
    thus ?case
      using "less.hyps"[OF _ ¬ q dvd p ¬ p dvd q]
      unfolding FW_sym[of p q] gcd.commute[of p q] add.commute[of p q] by blast
  next
    let ?d = "gcd p q"
    let ?dw = "[0..<(gcd p q)]"
    let ?pd = "p div (gcd p q)"
    assume "p < q"
    thus ?thesis
    proof (cases "?d = q - p")
      assume "?d = q - p" hence "p + ?d = q" using p < q by auto
      hence "p  q" and "¬ q < p" using p  0 p < q by fastforce+
      hence fw: "FW_word p q = fw_base p q"
        unfolding FW_word_def[of p q] using p  0  gcd p q = q - p by presburger


      have "|[0..<gcd p q]| = gcd p q"
        by simp
      hence *: "p div gcd p q * |[0..<gcd p q]| = p"
        by fastforce
      have ppref: "|butlast (?dw@?pd)[?d]| = p"
        using  p  0 unfolding lenmorph pow_len length_butlast sing_len * by fastforce
      note ppref' = this[unfolded lenmorph]
      have qpref: "|butlast (?dw@?pd)[?d]?dw| = q"
        unfolding lassoc lenmorph ppref' using  p + gcd p q = q by simp
      have "butlast (?dw@?pd)[?d] ≤p FW_word p q"
        unfolding fw fw_base_def fw_p_per_def lassoc  using triv_pref.
      from pref_take[OF this]
      have takep: "take p (FW_word p q) = butlast (?dw@?pd)[?d]"
        unfolding ppref.

      have "?dw  ε" and "|?dw| = ?d"
        using p  0 by auto
      have "?pd  0"
        by (simp add: p  0 dvd_div_eq_0_iff)
      from not0_implies_Suc[OF this]
      obtain e where "?pd = Suc e"  by blast
      have "gcd p q  p"
        using ¬ p dvd q gcd_dvd2[of p q] by force
      hence "Suc e  1"
        using dvd_mult_div_cancel[OF gcd_dvd1[of p q], unfolded ?pd = Suc e] by force
      hence "e  0" by simp

      have "[0..<gcd p q] @ e  ε"
        using [0..<gcd p q]  ε e  0 nonzero_pow_emp by blast
      hence but_dec: "butlast (?dw@?pd) = ?dw  butlast (?dw@e)"
        unfolding ?pd = Suc e pow_Suc butlast_append  if_not_P[OF [0..<gcd p q] @ e  ε] by blast
      have but_dec_b: "butlast (?dw@?pd) = ?dw@e  butlast ?dw"
        unfolding ?pd = Suc e pow_Suc' butlast_append if_not_P[OF ?dw  ε] by blast
      have "butlast (?dw@?pd)[?d]?dw ≤p FW_word p q"
        unfolding fw but_dec lassoc fw_base_def fw_p_per_def by blast
      note takeq = pref_take[OF this, unfolded qpref]

      have "|FW_word p q| = p + q - gcd p q - 1"
      proof-
        have "p + q - (q - p) = p + p"
          using p + gcd p q = q by auto
        hence "|?dw@?pd| = p"
           unfolding pow_len |[0..<gcd p q]| = gcd p q by force
        hence "|butlast (?dw@?pd)| = p - 1"
          unfolding length_butlast by argo
        hence "|FW_word p q| = (p - 1) + 1 +  (p - 1)"
          unfolding fw lenmorph sing_len fw_base_def fw_p_per_def by presburger
        thus "|FW_word p q| = p + q - gcd p q - 1"
          unfolding gcd p q = q - p p + q - (q - p) = p + p  using p  0 by fastforce
      qed

      have "period (FW_word p q) p"
        unfolding period_def
      proof (rule per_rootI)
        show "take p (FW_word p q)  ε"
          using p  0  unfolding length_0_conv[symmetric] ppref[folded takep].
        have "fw_base p q ≤p fw_p_per p q  [gcd p q]  fw_base p q"
          unfolding rassoc pref_cancel_conv fw_base_def fw_p_per_def by blast
        thus "FW_word p q ≤p take p (FW_word p q)  FW_word p q"
          unfolding fw rassoc fw_p_per_def takep[unfolded fw].
      qed

      have "period (FW_word p q) q"
        unfolding period_def
      proof (rule per_rootI)
        show "take q (FW_word p q)  ε"
          unfolding length_0_conv[symmetric] qpref[folded takeq] using p  0 p < q by linarith
        have "butlast ([0..<gcd p q] @ (p div gcd p q)) ≤p [0..<gcd p q]  butlast ([0..<gcd p q] @ (p div gcd p q))"
          using pref_prod_root[OF prefixeq_butlast[of "[0..<gcd p q] @ (p div gcd p q)"]].
        from pref_ext[OF this, unfolded rassoc]
        have "fw_base p q ≤p fw_p_per p q  [gcd p q]  [0..<gcd p q]  fw_base p q"
          unfolding rassoc pref_cancel_conv fw_base_def fw_p_per_def.
        thus "FW_word p q ≤p take q (FW_word p q)  FW_word p q"
          unfolding fw rassoc fw_p_per_def takeq[unfolded fw].
      qed

      have "¬ period (FW_word p q) ?d"
      proof-
        have last_a: "last (take p (FW_word p q)) = ?d"
          unfolding takep nth_append_length[of "butlast (?dw @ ?pd)" "?d" ε]
            last_snoc by blast
        have "?dw ≤p FW_word p q"
          unfolding fw but_dec rassoc fw_base_def fw_p_per_def by blast
        from pref_take[OF this, unfolded |?dw| = ?d]
        have takegcd:  "take (gcd p q) (FW_word p q) = [0..<gcd p q]".
        have fw_dec_b: "FW_word p q = [0..<gcd p q]@e  butlast ([0..<gcd p q])  [?d]  (butlast ([0..<gcd p q]@(p div gcd p q)))"
          unfolding fw but_dec_b rassoc fw_base_def fw_p_per_def ..
        have gcdepref:  "[0..<gcd p q]@ Suc e ≤p take (gcd p q) (FW_word p q)  FW_word p q"
          unfolding takegcd pow_Suc pref_cancel_conv unfolding fw_dec_b by blast
        have "|[0..<gcd p q]@ Suc e| = p"
          unfolding pow_len |?dw| = ?d ?pd = Suc e[symmetric] using
            dvd_div_mult_self[OF gcd_dvd1].
        from pref_take[OF gcdepref, unfolded this]
        have takegcdp:  "take p (take (gcd p q) (FW_word p q)  (FW_word p q)) = [0..<gcd p q]@e  [0..<gcd p q]"
          unfolding pow_Suc'.
        have "0 < gcd p q" by (simp add: p  0)
        from last_upt[OF this]
        have last_b: "last (take p (take (gcd p q) (FW_word p q)  (FW_word p q))) = gcd p q - 1"
          unfolding takegcdp  last_appendR[of "[0..<gcd p q]" "[0..<gcd p q]@e", OF [0..<gcd p q]  ε].
        have "p  |FW_word p q|"
          unfolding |FW_word p q| = p + q - gcd p q - 1 gcd p q = q - p using  p < q by auto
        have "gcd p q  gcd p q - 1"
          using gcd p q = q - p p < q by linarith
        hence "take p (FW_word p q)  take p (take (gcd p q) (FW_word p q)  (FW_word p q))"
          unfolding last_b[symmetric] unfolding last_a[symmetric] using arg_cong[of _ _ last] by blast
        hence "¬ FW_word p q ≤p take (gcd p q) (FW_word p q)  FW_word p q "
          using pref_share_take[OF _ p  |FW_word p q|, of "take (gcd p q) (FW_word p q)  FW_word p q"] by blast
        thus "¬ period (FW_word p q) (gcd p q)"
          unfolding period_def by blast
      qed

      show ?thesis
        using period (FW_word p q) p period (FW_word p q) q
          |FW_word p q| = p + q - gcd p q - 1 ¬ period (FW_word p q) (gcd p q) by blast
    next
      let ?d' = "gcd p (q-p)"
      assume "gcd p q  q - p"
      hence fw: "FW_word p q = (take p (FW_word p (q-p)))  FW_word p (q-p)"
        using FW_word_def p  0 p  q p < q by (meson less_Suc_eq not_less_eq)

      have divhyp1: "¬ p dvd q - p"
        using ¬ p dvd q p < q dvd_minus_self by auto

      have divhyp2: "¬ q - p dvd p"
      proof (rule notI)
        assume "q - p dvd p"
        have "q = p + (q - p)"
          by (simp add: p < q less_or_eq_imp_le)
        from gcd_add2[of p "q - p", folded  this, unfolded gcd_nat.absorb2[of "q - p" p, OF q - p dvd p]]
        show "False"
          using gcd p q  q - p by blast
      qed

      have lenhyp: "p + p + (q - p) < p + p + q"
        using p < q p  0 by linarith

― ‹induction assumption›
      have "|FW_word p (q - p)| = p + (q - p) - ?d' - 1" and "period (FW_word p (q-p)) p" and "period (FW_word p (q-p)) (q-p)" and
        "¬ period (FW_word p (q-p)) (gcd p (q-p))"
        using "less.hyps"[OF _ divhyp1 divhyp2] lenhyp
        by blast+

― ‹auxiliary facts›
      have "p + (q - p) = q"
         using divhyp1 dvd_minus_self by auto
      have "?d = ?d'"
        using  gcd_add2[of p "q-p", unfolded le_add_diff_inverse[OF less_imp_le[OF p < q]]].
      have "?d  q"
        using  ¬ q dvd p  gcd_dvd2[of q p, unfolded gcd.commute[of q]] by force
      from this[unfolded nat_neq_iff]
      have "?d < q"
        using  gr_implies_not0 p < q nat_dvd_not_less by blast
      hence "1  q - ?d"
        by linarith
      have "?d' < q - p"
        using  gcd_le2_pos[OF per_not_zero[OF period (FW_word p (q - p)) (q - p)], of p]  divhyp2[unfolded  gcd_nat.absorb_iff2] nat_less_le by blast
      hence "p  |(FW_word p (q - p))|"
        unfolding  |FW_word p (q - p)| = p + (q - p) - ?d' - 1 by linarith
      have "FW_word p (q - p)  ε"
        unfolding length_0_conv[symmetric] using  p  |FW_word p (q - p)| p  0[folded le_zero_eq]
        by linarith

― ‹claim 1›
      have "|FW_word p q| = p + q - ?d - 1"
      proof-
        have "p + (q - p) = q" using less_imp_le[OF p < q] by fastforce
        have "|FW_word p q| = |take p (FW_word p (q - p))| + |FW_word p (q - p)|"
          using fw lenmorph[of "take p (FW_word p (q - p))" "FW_word p (q - p)"]
          by presburger
        also have "... = p + (p + (q - p) - ?d' - 1)"
          unfolding |FW_word p (q - p)| = p + (q - p) - ?d' - 1
            take_len[OF p  |FW_word p (q - p)|] by blast
        also have "... = p + (q - ?d  - 1)"
          unfolding ?d = ?d' p + (q - p) = q..
        also have "... = p + (q - ?d) - 1"
          using Nat.add_diff_assoc[OF 1  q - ?d].
        also have "... = p + q - ?d - 1"
          by (simp add: ?d < q less_or_eq_imp_le)
        finally show "|FW_word p q| = p + q - ?d - 1"
          by presburger
      qed

― ‹claim 2›
      have "period (FW_word p q) p"
        using fw  ext_per_left[OF period (FW_word p (q-p)) p p  |FW_word p (q - p)|]
        by presburger

― ‹claim 3›
      have "period (FW_word p q) q"
        using ext_per_sum[OF period (FW_word p (q - p)) p period (FW_word p (q - p)) (q - p) p  |FW_word p (q - p)|, folded fw, unfolded p + (q-p) = q].

― ‹claim 4›
      have "¬ period (FW_word p q) ?d"
        using ¬ period (FW_word p (q -p)) (gcd p (q-p))
        unfolding ?d = ?d'[symmetric]
        using period_fac[of "take p (FW_word p (q - p))" "FW_word p (q - p)" ε "?d", unfolded append_Nil2,
                          OF _ FW_word p (q - p)  ε, folded fw] by blast
      thus ?thesis
        using period (FW_word p q) p period (FW_word p q) q |FW_word p q| = p + q - ?d - 1 by blast
    qed
  qed
qed

theorem fw_word: assumes "¬ p dvd q" "¬ q dvd p"
  shows "|FW_word p q| = p + q - gcd p q - 1" and "period (FW_word p q) p" and  "period (FW_word p q) q" and "¬ period (FW_word p q) (gcd p q)"
  using fw_word'[OF assms] by blast+

text‹Calculation examples›


section "Other variants of the periodicity lemma"

text ‹Periodicity lemma is one of the most frequent tools in Combinatorics on words.
   Here are some useful variants.›

text‹Note that the following lemmas are stronger versions of @{thm per_lemma_pref_suf fac_two_conjug_primroot fac_two_conjug_primroot' fac_two_conjug_primroot'' fac_two_prim_conjug} that have a relaxed length assumption @{term "|p| + |q|  |w|"} instead of @{term "|p| + |q| - (gcd |p| |q|)  |w|"} (and which follow from the relaxed version of periodicity lemma @{thm two_pers}.›


lemma per_lemma_pref_suf_gcd: assumes "w <p p  w" and "w <s w  q" and
  fw: "|p| + |q| - (gcd |p| |q|)  |w|"
obtains r s k l m where "p = (r  s)@k" and "q = (s  r)@l" and "w = (r  s)@m  r" and "primitive (rs)"
proof-
  let ?q = "(w  q)<¯w"
  have "w <p ?q  w"
    using ssufD1[OF w <s w  q] rq_suf[symmetric, THEN per_rootI[OF prefI rq_ssuf[OF w <s w  q]]]
    by argo
  have "q  ?q"
    by (meson assms(2) conjugI1 conjug_sym rq_suf suffix_order.less_imp_le)

  have nemps': "p  ε" "?q  ε"
    using assms(1) w <p ?qw by fastforce+
  have "|p| + |?q| - gcd (|p|) (|?q|)  |w|" using fw
    unfolding conjug_len[OF q  ?q].
  from per_lemma_comm[OF sprefD1[OF w <p p  w] sprefD1[OF w <p ?qw] this]
  have "p  ?q = ?q  p".
  then have "ρ p = ρ ?q" using comm_primroots[OF nemps'] by force
  hence [symmetric]: "ρ q  ρ p"
    using conjug_primroot[OF q  (w  q)<¯w]
    by argo
  from conjug_primrootsE[OF this]
  obtain r s k l where
    "p = (r  s) @ k" and
    "q = (s  r) @ l" and
    "primitive (r  s)".
  have "w ≤p (rs)w"
    using assms per_root_drop_exp  sprefD1 p = (r  s) @ k
    by meson
  have "w ≤s w(sr)"
    using assms(2) per_root_drop_exp[reversed] ssufD1 q = (s  r) @ l
    by meson
  have "|r  s|  |w|"
    using conjug_nemp_iff[OF q  ?q] dual_order.trans length_0_conv  nemps' per_lemma_len_le[OF fw] primroot_len_le[OF nemps'(1)]
    unfolding primroot_unique[OF nemps'(1) primitive (r  s) p = (r  s) @ k]
    by blast
  from root_suf_conjug[OF primitive (r  s) w ≤p (rs)w w ≤s w(sr) this]
  obtain m where "w = (r  s) @ m  r".
  from that[OF p = (r  s) @ k q = (s  r) @ l this primitive (r  s)]
  show ?thesis.
qed

lemma fac_two_conjug_primroot_gcd:
  assumes facs: "w ≤f p@k" "w ≤f q@l" and nemps: "p  ε" "q  ε" and len: "|p| + |q| - gcd (|p|) (|q|)  |w|"
  obtains r s m where "ρ p  r  s" and "ρ q  r  s" and "w = (r  s)@m  r" and "primitive (rs)"
proof -
  obtain p' where "w <p p'w" "p  p'" "p'  ε"
    using conjug_nemp_iff fac_pow_pref_conjug[OF facs(1)] nemps(1) per_rootI' by metis
  obtain q' where "w <s wq'" "q  q'" "q'  ε"
    using fac_pow_pref_conjug[reversed, OF w ≤f q@l] conjug_nemp_iff  nemps(2) per_rootI'[reversed] by metis
  from per_lemma_pref_suf_gcd[OF w <p p'w w <s wq']
  obtain r s k l m where
    "p' = (r  s) @ k" and
    "q' = (s  r) @ l" and
    "w = (r  s) @ m  r" and
    "primitive (r  s)"
    using len[unfolded conjug_len[OF p  p'] conjug_len[OF q  q']]
    by blast
  moreover have "ρ p' = rs"
    using p' = (r  s) @ k primitive (r  s) p'  ε primroot_unique by blast
  hence "ρ p  rs"
    using conjug_primroot[OF p  p']
    by simp
  moreover have "ρ q' = sr"
    using q' = (s  r) @ l primitive (r  s)[unfolded conjug_prim_iff'[of r]] q'  ε primroot_unique by blast
  hence "ρ q  sr"
    using conjug_primroot[OF q  q']  by simp
  hence "ρ q  rs"
    using conjug_trans[OF _ conjugI']
    by meson
  ultimately show ?thesis
    using that by blast
qed

corollary fac_two_conjug_primroot'_gcd:
   assumes facs: "u ≤f r@k" "u ≤f s@l" and nemps: "r  ε" "s  ε" and len: "|r| + |s| - gcd (|r|) (|s|)  |u|"
   shows "ρ r  ρ s"
  using fac_two_conjug_primroot_gcd[OF assms] conjug_trans[OF _ conjug_sym[of "ρ s"]].

lemma fac_two_conjug_primroot''_gcd:
  assumes facs: "u ≤f r@k" "u ≤f s@l" and "u  ε" and len: "|r| + |s| - gcd (|r|) (|s|)  |u|"
  shows "ρ r  ρ s"
proof -
  have nemps: "r  ε" "s  ε" using facs u  ε by auto
  show "conjugate (ρ r) (ρ s)" using fac_two_conjug_primroot'_gcd[OF facs nemps len].
qed

lemma  fac_two_prim_conjug_gcd:
  assumes "w ≤f u@n" "w ≤f v@m" "primitive u" "primitive v" "|u| + |v| - gcd (|u|) (|v|)  |w|"
  shows "u  v"
  using fac_two_conjug_primroot'_gcd[OF assms(1-2) _ _ assms(5)] prim_nemp[OF primitive u] prim_nemp[OF primitive v]
  unfolding prim_self_root[OF primitive u] prim_self_root[OF primitive v].

lemma two_pers_1:
  assumes pu: "w ≤p u  w" and pv: "w ≤p v  w" and len: "|u| + |v| - 1  |w|"
  shows "u  v = v  u"
proof
  assume "u  ε" "v  ε"
  hence "1  gcd |u| |v|"
    using nemp_len by (simp add: Suc_leI)
  thus ?thesis
    using per_lemma_comm[OF pu pv] len by linarith
qed


end