absurd H
case intro.intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
h_card : Fintype.card R = 1
x y : R
H : x ≠ y
⊢ False
case intro.intro
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
h_card : Fintype.card R = 1
x y : R
H : x ≠ y
⊢ x = y