rcases b with ⟨b, hb⟩
case right.mk
b : ↑VeryDiv
a : ℕ
ha : a ∈ VeryDiv
⊢ ↑{ val := a, property := ha } ∣ ↑b ∨ ↑b ∣ ↑{ val := a, property := ha }
case right.mk.mk
a : ℕ
ha : a ∈ VeryDiv
b : ℕ
hb : b ∈ VeryDiv
⊢ ↑{ val := a, property := ha } ∣ ↑{ val := b, property := hb } ∨
    ↑{ val := b, property := hb } ∣ ↑{ val := a, property := ha }