case zero
k : ℕ
h : k ≠ 0
⊢ factors zero <+ factors (zero * k)

case succ
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ factors (succ hn) <+ factors (succ hn * k)
n k : ℕ
h : k ≠ 0
⊢ factors n <+ factors (n * k)
cases' n with hn
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ factors (succ hn) <+~ factors (succ hn * k)
case succ
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ factors (succ hn) <+ factors (succ hn * k)
apply sublist_of_subperm_of_sorted _ (factors_sorted _) (factors_sorted _)
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ factors (succ hn) <+~ factors (succ hn) ++ factors k
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ factors (succ hn) <+~ factors (succ hn * k)
simp [(perm_factors_mul (Nat.succ_ne_zero _) h).subperm_left]
no goals
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ factors (succ hn) <+~ factors (succ hn) ++ factors k
exact (sublist_append_left _ _).subperm
no goals
case zero
k : ℕ
h : k ≠ 0
⊢ factors zero <+ factors (zero * k)
simp [zero_mul]