proposition: Lemma h_Zle_hnorm2 : (h h1) ^ 2 <= 4 * hnorm2 h1.
proof: Proof. destruct h1 ; intros ; unfold hnorm2, hmul, hconj. cbv delta [Hurwitz_def.h Hurwitz_def.i] ; cbv beta iota. apply Zle_0_minus_le ; ring_simplify. transitivity ((h + 2 * i) ^ 2 + (h + 2 * j) ^ 2 + (h + 2 * k) ^ 2). do 3 rewrite Zpower_2 ; repeat apply Zplus_le_0_compat ; apply Z.ge_le, sqr_pos. apply eq_Zle ; ring. Qed.
imports: ZArith Znumtheory Lia Zpow_facts MyZ Hurwitz_def