exact hAntisymm rxy (hEucl rxx rxy)
α : Type u
rel : α → α → Prop
hRefl✝ : Reflexive rel
hSymm : Symmetric rel
hSerial : Serial rel
hTrans : Transitive rel
hEucl✝ : Euclidean rel
hRefl : Reflexive rel
hAntisymm : Antisymmetric rel
hEucl : Euclidean rel
x y : α
rxy : rel x y
rxx : rel x x
⊢ x = y
no goals