Theorem: ne_min_of_ne_and_ne (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝¹ : Monad m
ι : Type u_1
inst✝ : LinearOrder ι
a x y : ι
hx : a ≠ x
hy : a ≠ y
⊢ a ≠ min x y
Tactic:
rcases min_choice x y with h | h <;> rw [h] <;> assumption
State after:
no goals