proposition: Lemma equivPrim_Op_DIV_Integer {Tl} : forall (t1 t2 : ArithExpr Tl Integer) (lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in eqExprTypePrim (evalPrim t1 lP) (evalRounded t1 lM mode_NE) -> eqExprTypePrim (evalPrim t2 lP) (evalRounded t2 lM mode_NE) -> (evalRounded t2 lM mode_NE <> 0)%Z -> - IZR (Int32.N / 2) <= IZR (Z.quot (evalRounded t1 lM mode_NE) (evalRounded t2 lM mode_NE)) <= IZR (Int32.N / 2 - 1) -> eqExprTypePrim (evalPrim (Op DIV t1 t2) lP) (evalRounded (Op DIV t1 t2) lM mode_NE).
proof: Proof. intros t1 t2 lP lM [bndt1 eqt1] [bndt2 eqt2] H0 [H1 H2]. rewrite <-opp_IZR in H1. apply le_IZR in H1, H2. unfold eqExprTypePrim. simpl in *. rewrite <-eqt1 in H1, H2 |- *. rewrite <-eqt2 in H0, H1, H2 |- *. assert (H: Sint63.to_Z (evalPrim t1 lP) <> Sint63.to_Z Sint63.min_int). { revert bndt1. unfold Int32.in_bounds. cbn -[evalPrim]. lia. } clear eqt1. now rewrite Sint63.div_spec; [| left]. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)