have h' := even_card_odd_degree_vertices G
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
h : Finset.card (filter (fun x => Odd (degree G x)) univ) = Fintype.card V
⊢ False
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
h : Finset.card (filter (fun x => Odd (degree G x)) univ) = Fintype.card V
h' : Even (Finset.card (filter (fun v => Odd (degree G v)) univ))
⊢ False