after_first_simp

c : ℕ,
h : c ≥ 3
⊢ c - 2 +
      int.nat_abs
        (2 +
           -↑(strong_induction_on 0
                  (λ (C2 : multiset ℕ) (HC : Π (t : multiset ℕ), t < C2 → multiset ℕ → ℕ)
                   (L : multiset ℕ),
                     strong_induction_on L
                       (λ (L2 : multiset ℕ) (HL : Π (t : multiset ℕ), t < L2 → ℕ),
                          N_min
                            (pmap (λ (a : ℕ) (h : a ∈ C2), a - 2 + int.nat_abs (2 + -↑(HC (erase C2 a) _ L2))) C2
                                 _ +
                               pmap (λ (a : ℕ) (h : a ∈ L2), a - 4 + int.nat_abs (4 + -↑(HL (erase L2 a) _))) L2
                                 _)))
                  0)) =
    c