proposition: Lemma equivPrim_Int {Tl} : forall n (lP : evalExprTypePrim_list Tl), (- Z.pow_pos 2 (Int32.bits - 1) <= n < Z.pow_pos 2 (Int32.bits - 1))%Z -> let lM := P2M_list lP in eqExprTypePrim (evalPrim (Int n) lP) (evalRounded (Int n) lM mode_NE).
proof: Proof. intros n lP H lM. unfold eqExprTypePrim. simpl. rewrite of_Z_spec. rewrite cmod_small; [| cbn in H |- *; lia]. split; [| easy]. revert H. unfold Int32.in_bounds. cbn. lia. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)