proposition: Lemma hconj_hminus : hconj (h1 h- h2) = (hconj h1) h- (hconj h2).
proof: Proof. unfold hminus, hadd, hopp, hconj ; destruct h1, h2 ; intros ; f_equal ; ring. Qed.
imports: ZArith Znumtheory Lia Zpow_facts MyZ Hurwitz_def