antisymmetry using (.≤.:Nat→Nat→Prop)
p : Nat → Bool
h : ∃ n, p n = true
this : (first p).leNat (bfind p h) = true
x : Nat
hle : x ≤ bfind p h
hx : p x = true
⊢ x = bfind p h
case a
p : Nat → Bool
h : ∃ n, p n = true
this : (first p).leNat (bfind p h) = true
x : Nat
hle : x ≤ bfind p h
hx : p x = true
⊢ x ≤ bfind p h

case a
p : Nat → Bool
h : ∃ n, p n = true
this : (first p).leNat (bfind p h) = true
x : Nat
hle : x ≤ bfind p h
hx : p x = true
⊢ bfind p h ≤ x