Pair Light Selected Floor Independent Bool eq prefix drop

import Init
import Mathlib.Data.List.Basic
import Definitions.Def_D1Bound5_PairLightArithmeticChunks_Definitions
import Definitions.Def_D1Bound5_PairLightArithmetic_Definitions

section
namespace D1Bound5


theorem _root_.D1Bound5.pairLightSelectedFloorIndependentBool_eq_prefix_drop
    (tau nu : Int) (sieve : List (Nat × Nat)) (n : Nat)
    (cached : List PairLightCachedVertex) (rows : List (Nat × List Nat)) :
    pairLightSelectedFloorIndependentBool tau nu sieve cached rows =
      (pairLightSelectedFloorPrefixBool tau nu sieve n cached rows &&
        pairLightSelectedFloorIndependentBool tau nu sieve (cached.drop n) (rows.drop n)) := by sorry





end D1Bound5
end