norm_num at hcon
case refine_2
α : Type u_1
M N : Matroid α
e✝ f✝ g : α
I X P D : Set α
h : ∀ (C : Set α), M.Circuit C → 3 ≤ C.encard
e f : α
hef : M.Parallel e f
hne : ¬e = f
hcon : 3 ≤ 2
⊢ False
no goals