Theory Polynomial_Interpolation.Missing_Unsorted

(*  
    Author:      René Thiemann 
                 Akihisa Yamada
                 Jose Divason
    License:     BSD
*)
section ‹Missing Unsorted›

text ‹This theory contains several lemmas which might be of interest to the Isabelle distribution.
  For instance, we prove that $b^n \cdot n^k$ is bounded by a constant whenever $0 < b < 1$.›

theory Missing_Unsorted
imports
  Complex_Main "HOL-Computational_Algebra.Factorial_Ring"
begin

context
  fixes b :: "'a :: archimedean_field"
  assumes b: "0 < b" "b < 1"
begin

lemma exp_tends_to_zero: 
  assumes c: "c > 0"
  shows "∃ x. b ^ x ≤ c" 
proof (rule ccontr)
  assume not: "¬ ?thesis"
  define bb where "bb = inverse b"
  define cc where "cc = inverse c"
  from b have bb: "bb > 1" unfolding bb_def by (rule one_less_inverse)  
  from c have cc: "cc > 0" unfolding cc_def by simp
  define bbb where "bbb = bb - 1"
  have id: "bb = 1 + bbb" and bbb: "bbb > 0" and bm1: "bbb ≥ -1" unfolding bbb_def using bb by auto
  have "∃ n. cc / bbb < of_nat n" by (rule reals_Archimedean2)
  then obtain n where lt: "cc / bbb < of_nat n" by auto
  from not have "¬ b ^ n ≤ c" by auto
  hence bnc: "b ^ n > c" by simp
  have "bb ^ n = inverse (b ^ n)" unfolding bb_def by (rule power_inverse)
  also have "… < cc" unfolding cc_def
    by (rule less_imp_inverse_less[OF bnc c])
  also have "… < bbb * of_nat n" using lt bbb by (metis mult.commute pos_divide_less_eq)
  also have "… ≤ bb ^ n"
    using Bernoulli_inequality[OF bm1, folded id, of n] by (simp add: ac_simps)
  finally show False by simp
qed

lemma linear_exp_bound: "∃ p. ∀ n. b ^ n * of_nat n ≤ p"
proof -
  obtain n0 where x0: "b ^ n0 ≤ 1 - b"
    using b exp_tends_to_zero by fastforce
  have *: "b ^ n ≤ 1 - b" if "n ≥ n0" for n
   by (metis that b order_trans power_decreasing_iff x0)
  define bs where "bs ≡ insert 1 ((λn. b ^ Suc n * of_nat (Suc n)) ` {..n0})"
  have "finite bs" unfolding bs_def by auto
  define p where "p = Max bs"
  have bs: "⋀ b. b ∈ bs ⟹ b ≤ p"
    by (simp add: ‹finite bs› p_def)
  hence p1: "p ≥ 1" unfolding bs_def by auto
  show ?thesis
  proof (intro allI exI)
    fix n
    show "b ^ n * of_nat n ≤ p"
    proof (induct n)
      case (Suc n)
      show ?case
      proof (cases "n ≤ n0")
        case True
        with bs show ?thesis 
          by (auto simp: bs_def)
      next
        case False
        let ?x = "of_nat n :: 'a"
        have "b ^ (Suc n) * of_nat (Suc n) = b * (b ^ n * ?x) + b ^ Suc n" by (simp add: field_simps)
        also have "… ≤ b * p + b ^ Suc n"
          using b by (intro add_right_mono[OF mult_left_mono[OF Suc]]) auto
        also have "… = p - ((1 - b) * p - b ^ (Suc n))" by (simp add: field_simps)
        also have "… ≤ p - 0"
        proof -
          have "b ^ Suc n ≤ 1 - b" using *[of "Suc n"] False by auto
          also have "… ≤ (1 - b) * p" using b p1 by auto
          finally show ?thesis
            by (intro diff_left_mono, simp)
        qed
        finally show ?thesis by simp
      qed
    qed (use p1 in auto)
  qed
qed

lemma poly_exp_bound: "∃ p. ∀ n. b ^ n * of_nat n ^ deg ≤ p" 
proof -
  show ?thesis
  proof (induct deg)
    case 0
    show ?case
      using b power_decreasing_iff by auto
  next
    case (Suc deg)
    then obtain q where IH: "⋀ x. b ^ x * (of_nat x) ^ deg ≤ q" by auto
    define p where "p = max 0 q"
    from IH have IH: "⋀ x. b ^ x * (of_nat x) ^ deg ≤ p" unfolding p_def using le_max_iff_disj by blast
    have p: "p ≥ 0" unfolding p_def by simp
    show ?case
    proof (cases "deg = 0")
      case True
      thus ?thesis using linear_exp_bound by simp
    next
      case False note deg = this
      define p' where "p' = p*p * 2 ^ Suc deg * inverse b"
      let ?f = "λ x. b ^ x * (of_nat x) ^ Suc deg"
      define f where "f = ?f"
      {
        fix x
        let ?x = "of_nat x :: 'a"
        have "f (2 * x) ≤ (2 ^ Suc deg) * (p * p)"
        proof (cases "x = 0")
          case False
          hence x1: "?x ≥ 1" by (cases x, auto)
          from x1 have x: "?x ^ (deg - 1) ≥ 1" by simp
          from x1 have xx: "?x ^ Suc deg ≥ 1" by (rule one_le_power)
          define c where "c = b ^ x * b ^ x * (2 ^ Suc deg)"
          have c: "c > 0" unfolding c_def using b by auto
          have "f (2 * x) = ?f (2 * x)" unfolding f_def by simp
          also have "b ^ (2 * x) = (b ^ x) * (b ^ x)" by (simp add: power2_eq_square power_even_eq)
          also have "of_nat (2 * x) = 2 * ?x" by simp
          also have "(2 * ?x) ^ Suc deg = 2 ^ Suc deg * ?x ^ Suc deg" by simp
          finally have "f (2 * x) = c * ?x ^ Suc deg" unfolding c_def by (simp add: ac_simps)
          also have "… ≤ c * ?x ^ Suc deg * ?x ^ (deg - 1)"
          proof -
            have "c * ?x ^ Suc deg > 0" using c xx by simp
            thus ?thesis unfolding mult_le_cancel_left1 using x by simp
          qed
          also have "… = c * ?x ^ (Suc deg + (deg - 1))" by (simp add: power_add)
          also have "Suc deg + (deg - 1) = deg + deg" using deg by simp
          also have "?x ^ (deg + deg) = (?x ^ deg) * (?x ^ deg)" by (simp add: power_add)
          also have "c * … = (2 ^ Suc deg) * ((b ^ x * ?x ^ deg) * (b ^ x * ?x ^ deg))" 
            unfolding c_def by (simp add: ac_simps)  
          also have "… ≤ (2 ^ Suc deg) * (p * p)"
            using mult_left_mono[OF mult_mono[OF IH IH p]] b by fastforce
          finally show "f (2 * x) ≤ (2 ^ Suc deg) * (p * p)" .
        qed (auto simp: f_def)
        hence "?f (2 * x) ≤ (2 ^ Suc deg) * (p * p)" unfolding f_def .
      } note even = this
      show ?thesis
      proof (rule exI[of _ p'], intro allI)
        fix y
        show "?f y ≤ p'"
        proof (cases "even y")
          case True
          define x where "x = y div 2"
          have "y = 2 * x" unfolding x_def using True by simp
          from even[of x, folded this] have "?f y ≤ 2 ^ Suc deg * (p * p)" .
          also have "… ≤ … * inverse b"
            unfolding mult_le_cancel_left1 using b p
            by (simp add: algebra_split_simps one_le_inverse)
          also have "… = p'" unfolding p'_def by (simp add: ac_simps)
          finally show "?f y ≤ p'" .
        next
          case False
          define x where "x = y div 2"
          have "y = 2 * x + 1" unfolding x_def using False by simp
          hence "?f y = ?f (2 * x + 1)" by simp
          also have "… ≤ b ^ (2 * x + 1) * of_nat (2 * x + 2) ^ Suc deg"
            by (rule mult_left_mono[OF power_mono], insert b, auto) 
          also have "b ^ (2 * x + 1) = b ^ (2 * x + 2) * inverse b" using b by auto
          also have "b ^ (2 * x + 2) * inverse b * of_nat (2 * x + 2) ^ Suc deg = 
            inverse b * ?f (2 * (x + 1))" by (simp add: ac_simps)
          also have "… ≤ inverse b * ((2 ^ Suc deg) * (p * p))"
            by (rule mult_left_mono[OF even], insert b, auto)
          also have "… = p'" unfolding p'_def by (simp add: ac_simps)
          finally show "?f y ≤ p'" .
        qed
      qed
    qed
  qed
qed

end

lemma set_upt_Suc: "{0 ..< Suc i} = insert i {0 ..< i}"
  by (fact atLeast0_lessThan_Suc)


(* GCD and LCM part *)

lemma dvd_abs_mult_left_int [simp]:
  "¦a¦ * y dvd x ⟷ a * y dvd x" for x y a :: int
  using abs_dvd_iff [of "a * y"] abs_dvd_iff [of "¦a¦ * y"]
  by (simp add: abs_mult)
  
lemma gcd_abs_mult_right_int [simp]:
  "gcd x (¦a¦ * y) = gcd x (a * y)" for x y a :: int
  using gcd_abs2_int [of _ "a * y"] gcd_abs2_int [of _ "¦a¦ * y"]
  by (simp add: abs_mult)

lemma lcm_abs_mult_right_int [simp]:
  "lcm x (¦a¦ * y) = lcm x (a * y)" for x y a :: int
  using lcm_abs2_int [of _ "a * y"] lcm_abs2_int [of _ "¦a¦ * y"]
  by (simp add: abs_mult)

lemma gcd_abs_mult_left_int [simp]:
  "gcd x (a * ¦y¦) = gcd x (a * y)" for x y a :: int
  using gcd_abs2_int [of _ "a * ¦y¦"] gcd_abs2_int [of _ "a * y"]
  by (simp add: abs_mult)

lemma lcm_abs_mult_left_int [simp]:
  "lcm x (a * ¦y¦) = lcm x (a * y)" for x y a :: int
  using lcm_abs2_int [of _ "a * ¦y¦"] lcm_abs2_int [of _ "a * y"]
  by (simp add: abs_mult)


abbreviation (input) list_gcd :: "'a :: semiring_gcd list ⇒ 'a" where
  "list_gcd ≡ gcd_list"

abbreviation (input) list_lcm :: "'a :: semiring_gcd list ⇒ 'a" where
  "list_lcm ≡ lcm_list"


lemma list_gcd_simps: "list_gcd [] = 0" "list_gcd (x # xs) = gcd x (list_gcd xs)"
  by simp_all

lemma list_gcd: "x ∈ set xs ⟹ list_gcd xs dvd x"
  by (fact Gcd_fin_dvd)

lemma list_gcd_greatest: "(⋀ x. x ∈ set xs ⟹ y dvd x) ⟹ y dvd (list_gcd xs)"
  by (fact gcd_list_greatest)

lemma list_gcd_mult_int [simp]: 
  fixes xs :: "int list"
  shows "list_gcd (map (times a) xs) = ¦a¦ * list_gcd xs"
  by (simp add: Gcd_mult abs_mult)

lemma list_lcm_simps: "list_lcm [] = 1" "list_lcm (x # xs) = lcm x (list_lcm xs)"
  by simp_all

lemma list_lcm: "x ∈ set xs ⟹ x dvd list_lcm xs" 
  by (fact dvd_Lcm_fin)

lemma list_lcm_least: "(⋀ x. x ∈ set xs ⟹ x dvd y) ⟹ list_lcm xs dvd y"
  by (fact lcm_list_least)

lemma lcm_mult_distrib_nat: "(k :: nat) * lcm m n = lcm (k * m) (k * n)"
  by (simp add: lcm_mult_left)

lemma lcm_mult_distrib_int: "abs (k::int) * lcm m n = lcm (k * m) (k * n)"
  by (simp add: lcm_mult_left abs_mult)

lemma list_lcm_mult_int [simp]:
  fixes xs :: "int list"
  shows "list_lcm (map (times a) xs) = (if xs = [] then 1 else ¦a¦ * list_lcm xs)"
  by (simp add: Lcm_mult abs_mult)

lemma list_lcm_pos:
  "list_lcm xs ≥ (0 :: int)"
  "0 ∉ set xs ⟹ list_lcm xs ≠ 0"
  "0 ∉ set xs ⟹ list_lcm xs > 0" 
proof -
  have "0 ≤ ¦Lcm (set xs)¦"
    by (simp only: abs_ge_zero)
  then have "0 ≤ Lcm (set xs)"
    by simp
  then show "list_lcm xs ≥ 0"
    by simp
  assume "0 ∉ set xs"
  then show "list_lcm xs ≠ 0"
    by (simp add: Lcm_0_iff)
  with ‹list_lcm xs ≥ 0› show "list_lcm xs > 0"
    by (simp add: le_less)
qed

lemma quotient_of_nonzero: "snd (quotient_of r) > 0" "snd (quotient_of r) ≠ 0"
  using quotient_of_denom_pos' [of r] by simp_all

lemma quotient_of_int_div: 
  assumes q: "quotient_of (of_int x / of_int y) = (a, b)"
  and y: "y ≠ 0" 
  shows "∃ z. z ≠ 0 ∧ x = a * z ∧ y = b * z"
proof -
  let ?r = "rat_of_int"
  define z where "z = gcd x y"
  define x' where "x' = x div z"
  define y' where "y' = y div z"
  have id: "x = z * x'" "y = z * y'" unfolding x'_def y'_def z_def by auto
  from y have y': "y' ≠ 0" unfolding id by auto
  have z: "z ≠ 0" unfolding z_def using y by auto
  have cop: "coprime x' y'" unfolding x'_def y'_def z_def 
    using div_gcd_coprime y by blast
  have "?r x / ?r y = ?r x' / ?r y'" unfolding id using z y y' by (auto simp: field_simps) 
  from assms[unfolded this] have quot: "quotient_of (?r x' / ?r y') = (a, b)" by auto
  from quotient_of_coprime[OF quot] have cop': "coprime a b" .
  hence cop: "coprime b a"
    by (simp add: ac_simps)
  from quotient_of_denom_pos[OF quot] have b: "b > 0" "b ≠ 0" by auto
  from quotient_of_div[OF quot] quotient_of_denom_pos[OF quot] y'
  have "?r x' * ?r b = ?r a * ?r y'" by (auto simp: field_simps)
  hence id': "x' * b = a * y'" unfolding of_int_mult[symmetric] by linarith
  from id'[symmetric] have "b dvd y' * a" unfolding mult.commute[of y'] by auto
  with cop y' have "b dvd y'"
    by (simp add: coprime_dvd_mult_left_iff) 
  then obtain z' where ybz: "y' = b * z'" unfolding dvd_def by auto
  from id[unfolded y' this] have y: "y = b * (z * z')" by auto
  with ‹y ≠ 0› have zz: "z * z' ≠ 0" by auto
  from quotient_of_div[OF q] ‹y ≠ 0› ‹b ≠ 0› 
  have "?r x * ?r b = ?r y * ?r a" by (auto simp: field_simps)
  hence id': "x * b = y * a" unfolding of_int_mult[symmetric] by linarith
  from this[unfolded y] b have x: "x = a * (z * z')" by auto
  show ?thesis unfolding x y using zz by blast
qed

fun max_list_non_empty :: "('a :: linorder) list ⇒ 'a" where
  "max_list_non_empty [x] = x"
| "max_list_non_empty (x # xs) = max x (max_list_non_empty xs)"

lemma max_list_non_empty: "x ∈ set xs ⟹ x ≤ max_list_non_empty xs"
proof (induct xs)
  case (Cons y ys) note oCons = this
  show ?case 
  proof (cases ys)
    case (Cons z zs)
    hence id: "max_list_non_empty (y # ys) = max y (max_list_non_empty ys)" by simp
    from oCons show ?thesis unfolding id by (auto simp: max.coboundedI2)
  qed (insert oCons, auto)
qed simp

lemma cnj_reals[simp]: "(cnj c ∈ ℝ) = (c ∈ ℝ)"
  using Reals_cnj_iff by fastforce

lemma sgn_real_mono: "x ≤ y ⟹ sgn x ≤ sgn (y :: real)"
  unfolding sgn_real_def
  by (auto split: if_splits)

lemma sgn_minus_rat: "sgn (- (x :: rat)) = - sgn x"
  by (fact Rings.sgn_minus)

lemma real_of_rat_sgn: "sgn (of_rat x) = real_of_rat (sgn x)"
  unfolding sgn_real_def sgn_rat_def by auto

lemma inverse_le_iff_sgn: 
  assumes sgn: "sgn x = sgn y"
  shows "(inverse (x :: real) ≤ inverse y) = (y ≤ x)"
  by (metis inverse_le_imp_le inverse_le_imp_le_neg linorder_not_less nle_le sgn sgn_0_0 sgn_le_0_iff)

lemma inverse_le_sgn: 
  assumes sgn: "sgn x = sgn y" and xy: "x ≤ (y :: real)"
  shows "inverse y ≤ inverse x"
  using xy inverse_le_iff_sgn[OF sgn] by auto

lemma set_list_update: "set (xs [i := k]) = 
  (if i < length xs then insert k (set (take i xs) ∪ set (drop (Suc i) xs)) else set xs)"
  by (simp add: leI list_update_beyond set_list_update)

lemma dvd_prod:
fixes A::"'b set" 
assumes "∃b∈A. a dvd f b" "finite A"
shows "a dvd prod f A" 
using assms(2,1)
proof (induct A)
  case (insert x A)
  thus ?case 
    using comm_monoid_mult_class.dvd_mult dvd_mult2 insert_iff prod.insert by auto
qed auto

context
  fixes xs :: "'a :: comm_monoid_mult list"
begin
lemma prod_list_filter: "prod_list (filter f xs) * prod_list (filter (λ x. ¬ f x) xs) = prod_list xs"
  by (induct xs, auto simp: ac_simps)

lemma prod_list_partition: assumes "partition f xs = (ys, zs)"
  shows "prod_list xs = prod_list ys * prod_list zs"
  using assms by (subst prod_list_filter[symmetric, of f], auto simp: o_def)
end

lemma dvd_imp_mult_div_cancel_left[simp]:
  assumes "(a :: 'a :: semidom_divide) dvd b"
  shows "a * (b div a) = b"
  using assms nonzero_mult_div_cancel_left by fastforce

lemma (in semidom) prod_list_zero_iff[simp]: 
  "prod_list xs = 0 ⟷ 0 ∈ set xs" by (induction xs, auto)


context comm_monoid_mult begin

lemma unit_prod [intro]:
  shows "a dvd 1 ⟹ b dvd 1 ⟹ (a * b) dvd 1"
  by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono)

lemma is_unit_mult_iff[simp]:
  shows "(a * b) dvd 1 ⟷ a dvd 1 ∧ b dvd 1"
  by (auto dest: dvd_mult_left dvd_mult_right)

end

context comm_semiring_1
begin
lemma irreducibleE[elim]:
  assumes "irreducible p"
      and "p ≠ 0 ⟹ ¬ p dvd 1 ⟹ (⋀a b. p = a * b ⟹ a dvd 1 ∨ b dvd 1) ⟹ thesis"
  shows thesis using assms by (auto simp: irreducible_def)

lemma not_irreducibleE:
  assumes "¬ irreducible x"
      and "x = 0 ⟹ thesis"
      and "x dvd 1 ⟹ thesis"
      and "⋀a b. x = a * b ⟹ ¬ a dvd 1 ⟹ ¬ b dvd 1 ⟹ thesis"
  shows thesis using assms unfolding irreducible_def by auto

lemma prime_elem_dvd_prod_list:
  assumes p: "prime_elem p" and pA: "p dvd prod_list A" shows "∃a ∈ set A. p dvd a"
  using pA
proof(induct A)
  case Nil
  with p show ?case by (simp add: prime_elem_not_unit)
next
  case (Cons a A)
  then show ?case by (auto simp: prime_elem_dvd_mult_iff[OF p])
qed

lemma prime_elem_dvd_prod_mset:
  assumes p: "prime_elem p" and pA: "p dvd prod_mset A" shows "∃a ∈# A. p dvd a"
  using pA
proof(induct A)
  case empty
  with p show ?case by (simp add: prime_elem_not_unit)
next
  case (add a A)
  then show ?case by (auto simp: prime_elem_dvd_mult_iff[OF p])
qed

lemma mult_unit_dvd_iff[simp]:
  assumes "b dvd 1"
  shows "a * b dvd c ⟷ a dvd c"
  by (metis assms dvd.dvdE local.dvd_mult_left local.dvd_refl local.mult_dvd_mono local.one_dvd)

lemma mult_unit_dvd_iff'[simp]: "a dvd 1 ⟹ (a * b) dvd c ⟷ b dvd c"
  using mult_unit_dvd_iff [of a b c] by (simp add: ac_simps)

lemma irreducibleD':
  assumes "irreducible a" "b dvd a"
  shows   "a dvd b ∨ b dvd 1"
proof -
  from assms obtain c where c: "a = b * c" by (elim dvdE)
  from irreducibleD[OF assms(1) this] have "b dvd 1 ∨ c dvd 1" .
  thus ?thesis by (auto simp: c)
qed

end



context idom
begin

text ‹
  Following lemmas are adapted and generalized so that they don't use "algebraic" classes.
›

lemma dvd_times_left_cancel_iff [simp]:
  assumes "a ≠ 0"
  shows "a * b dvd a * c ⟷ b dvd c"
    (is "?lhs ⟷ ?rhs")
  using assms local.dvd_mult_cancel_left by presburger

lemma dvd_times_right_cancel_iff [simp]:
  assumes "a ≠ 0"
  shows "b * a dvd c * a ⟷ b dvd c"
  using assms local.dvd_mult_cancel_right by presburger

lemma irreducibleI':
  assumes "a ≠ 0" "¬ a dvd 1" "⋀b. b dvd a ⟹ a dvd b ∨ b dvd 1"
  shows   "irreducible a"
  unfolding irreducible_def
  by (metis assms dvd_times_left_cancel_iff local.dvd_triv_left local.mult_cancel_left1)

lemma irreducible_altdef:
  shows "irreducible x ⟷ x ≠ 0 ∧ ¬ x dvd 1 ∧ (∀b. b dvd x ⟶ x dvd b ∨ b dvd 1)"
  using local.irreducibleD' irreducibleI' irreducible_def by blast

lemma dvd_mult_unit_iff:
  assumes "b dvd 1"
  shows "a dvd c * b ⟷ a dvd c"
  by (meson assms local.dvd_refl local.dvd_trans local.mult_unit_dvd_iff)

lemma dvd_mult_unit_iff': "b dvd 1 ⟹ a dvd b * c ⟷ a dvd c"
  using dvd_mult_unit_iff [of b a c] by (simp add: ac_simps)

lemma irreducible_mult_unit_left:
  shows "a dvd 1 ⟹ irreducible (a * p) ⟷ irreducible p"
  by (auto simp: irreducible_altdef mult.commute[of a] dvd_mult_unit_iff)

lemma irreducible_mult_unit_right:
  shows "a dvd 1 ⟹ irreducible (p * a) ⟷ irreducible p"
  by (auto simp: irreducible_altdef mult.commute[of a] dvd_mult_unit_iff)

lemma prime_elem_imp_irreducible:
  assumes "prime_elem p"
  shows   "irreducible p"
proof (rule irreducibleI)
  fix a b
  assume p_eq: "p = a * b"
  with assms have nz: "a ≠ 0" "b ≠ 0" by auto
  from p_eq have "p dvd a * b" by simp
  with ‹prime_elem p› have "p dvd a ∨ p dvd b" by (rule prime_elem_dvd_multD)
  with ‹p = a * b› have "a * b dvd 1 * b ∨ a * b dvd a * 1" by auto
  with nz show "a dvd 1 ∨ b dvd 1"
    using local.dvd_mult_cancel_right local.dvd_times_left_cancel_iff by blast
qed (insert assms, simp_all add: prime_elem_def)

lemma unit_imp_dvd [dest]: "b dvd 1 ⟹ b dvd a"
  by (rule dvd_trans [of _ 1]) simp_all

lemma unit_mult_left_cancel: "a dvd 1 ⟹ a * b = a * c ⟷ b = c"
  using mult_cancel_left [of a b c] by auto

lemma unit_mult_right_cancel: "a dvd 1 ⟹ b * a = c * a ⟷ b = c"
  using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps)

end

lemma (in field) irreducible_field[simp]:
  "irreducible x ⟷ False" by (auto simp: dvd_field_iff irreducible_def)

lemma (in idom) irreducible_mult:
  shows "irreducible (a*b) ⟷ a dvd 1 ∧ irreducible b ∨ b dvd 1 ∧ irreducible a"
  by (auto dest: irreducible_multD simp: irreducible_mult_unit_left irreducible_mult_unit_right)


end