proposition: Lemma in_bounds_norm : forall n, in_bounds (norm n).
proof: Proof. intros n. unfold in_bounds, norm. replace (N / 2)%Z with (N - N / 2)%Z at 2. { apply cmod_bounded. now apply Zpower_pos_gt_0. } unfold N. rewrite Z.pow_pos_fold. replace (Z.pos bits) with (Z.pos bits - 1 + 1)%Z at 1 by ring. rewrite Z.pow_add_r ; [|lia|easy]. rewrite Z.pow_sub_r ; [|easy|lia]. change (2 ^ 1)%Z with 2%Z. ring. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)