proposition: Lemma real_hnorm2 : is_real (hmul h1 (hconj h1)).
proof: Proof. destruct h1 ; intros; unfold hmul, hconj. repeat split; cbv delta [Hurwitz_def.h Hurwitz_def.i Hurwitz_def.j Hurwitz_def.k]; cbv iota beta; ring. Qed.
imports: ZArith Znumtheory Lia Zpow_facts MyZ Hurwitz_def