An Interactive Algebra Course with Formalised Proofs and Definitions