α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b a : α
⊢ ￢￢a ≤ a
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b a : α
⊢ ￢￢a ⊔ ∂ a = a
rw [boundary, sup_inf_left, hnot_sup_self, inf_top_eq, sup_eq_right]
no goals
α : Type u_1
inst✝ : CoheytingAlgebra α
a✝ b a : α
⊢ ￢￢a ≤ a
exact hnot_hnot_le