proposition: Lemma equivFloat_Int {Tl} : forall n (lC : evalExprTypeFloat_list Tl) md, (- Z.pow_pos 2 (Int32.bits - 1) <= n < Z.pow_pos 2 (Int32.bits - 1))%Z -> let lM := C2M_list lC in eqExprTypeFloat (evalFloat (Int n) lC md) (evalRounded (Int n) lM md).
proof: Proof. intros n lC md H lM. simpl. split; [apply Int32.in_bounds_norm | apply Int32.norm_in_bounds]. unfold Int32.in_bounds, Int32.N. unfold Int32.bits. revert H. cbn. lia. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)