proposition: Lemma norm_in_bounds : forall n, in_bounds n -> norm n = n.
proof: Proof. intros n. unfold in_bounds, norm. rewrite cmod_cmod by now apply Zpower_pos_gt_0. intros H. apply Sint63.cmod_small. lia. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)