refactor(algebra/quaternion): remove `quaternion.conj` (#18803)
Instead we use `star` directly. We keep only the lemmas that refer to quaternion-specific operators, as the rest are already covered by the star API.
In practice, this is mostly the lemmas about the real and imaginary parts of quaternions.
The `commute_self_conj` lemma has been replaced by a `is_star_normal` instance.
