Data.List.Intervals mathlib4#1479

Stream: mathlib4

[Johan Commelin]

This PR contains

theorem bagInter_consecutive (n m l : Nat) : @List.bagInter ℕ instBEq (Ico n m) (Ico m l) = [] :=

and the explicit instance is needed because

example : instBEqNat = instBEq := rfl --fails

Shall we just add a porting note and move on?