∀ {α : Type u_1} [inst : CommMonoidWithZero α] (motive : (x x_1 : Associates.FactorSet α) → x ≤ x_1 → Prop)
  (x x_1 : Associates.FactorSet α) (x_2 : x ≤ x_1),
  (∀ (b : Associates.FactorSet α) (h : ⊤ ≤ b), motive none b h) →
    (∀ (a : Associates.FactorSet α) (x : a ≤ ⊤), motive a none x) →
      (∀ (val val_1 : Multiset { a // Irreducible a }) (h : ↑val ≤ ↑val_1), motive (some val) (some val_1) h) →
        motive x x_1 x_2