proposition: Lemma is_H_unit_hnorm2_1 : forall x, is_H_unit x -> hnorm2 x = 1.
proof: Proof. intros x (y, Ixy). assert (H : hnorm2 x * hnorm2 y = 1). etransitivity ; [symmetry ; eapply hnorm2_hmul |]. rewrite Ixy ; apply hnorm2_IZH. eapply Zmult_one ; [apply Z.le_ge, hnorm2_pos | eassumption]. Qed.
imports: ZArith Znumtheory Lia Zpow_facts MyZ Hurwitz_def