proposition: Lemma equivFloat_Op_DIV_Integer {Tl} : forall (t1 t2 : ArithExpr Tl Integer) (lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in eqExprTypeFloat (evalFloat t1 lC md) (evalRounded t1 lM md) -> eqExprTypeFloat (evalFloat t2 lC md) (evalRounded t2 lM md) -> (evalRounded t2 lM md <> 0)%Z -> - IZR (Int32.N / 2) <= IZR (Z.quot (evalRounded t1 lM md) (evalRounded t2 lM md)) <= IZR (Int32.N / 2 - 1) -> eqExprTypeFloat (evalFloat (Op DIV t1 t2) lC md) (evalRounded (Op DIV t1 t2) lM md).
proof: Proof. intros t1 t2 lC md lM [bndt1 eqt1] [bndt2 eqt2] H0 [H1 H2]. rewrite <-opp_IZR in H1. apply le_IZR in H1, H2. unfold eqExprTypeFloat. simpl. rewrite eqt1, eqt2. split; [apply Int32.in_bounds_norm | now apply Int32.norm_in_bounds]. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)