rw [decide_eq_false_iff_not]
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
h : (Fin.find? fun b => decide (Setoid.r i b)) = none
⊢ ¬decide (Setoid.r i i) = false
n : Nat
s : Setoid (Fin n)
inst✝ : DecidableRel Setoid.r
i j : Fin n
hij : Setoid.r i j
h : (Fin.find? fun b => decide (Setoid.r i b)) = none
⊢ ¬¬Setoid.r i i