feat(order/symm_diff): Heyting bi-implication (#16544)
Define `bihimp`, the Heyting bi-implication operator. This is dual to `symm_diff` and generalizes `iff` on propositions.
Delete `order.imp` as all the material there is now fully superseded by the Heyting algebra material (`himp`, defined in `order.heyting.basic`).
