feat(order/heyting_algebra): Heyting algebras (#15305)
Define (generalized) Heyting, co-Heyting and bi-Heyting algebras.
No lemma has been renamed, even though this might look like so from the diff.
`himp` is now a field of `boolean_algebra`, with default value `λ x y, y ⊔ xᶜ`.
## Duplicated lemmas
Those lemmas have been duplicated because they are true for Heyting algebras but are also used to prove that Boolean algebras are Heyting algebras:
* `sdiff_le'`
* `inf_compl_eq_bot'`
## Changes to argument implicitness
* `sdiff_inf_self_left`
* `sdiff_inf_self_right`
