simp_rw [VeryDiv] at *
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 }
case right.mk.mk
a : ℕ
ha : a ∈ {1, 2, 6, 30, 210}
b : ℕ
hb : b ∈ {1, 2, 6, 30, 210}
⊢ a ∣ b ∨ b ∣ a