proposition: Lemma Ztrunc_div_ : forall x y : Z, Ztrunc (IZR x / IZR y) = (x ÷ y)%Z.
proof: Proof. intros x y. destruct (Zeq_bool y 0) eqn:Hy; [apply Zeq_bool_eq in Hy | apply Zeq_bool_neq in Hy]. - rewrite Hy. unfold Rdiv. now rewrite Rinv_0, Rmult_0_r, Zquot.Zquot_0_r, Ztrunc_IZR. - now apply Ztrunc_div. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)