proposition: Theorem Zfloor_div : forall x y, y <> Z0 -> Zfloor (IZR x / IZR y) = (x / y)%Z.
proof: Proof. intros x y Zy. generalize (Z.div_mod x y Zy). intros Hx. rewrite Hx at 1. assert (Zy': IZR y <> 0%R). contradict Zy. now apply eq_IZR. unfold Rdiv. rewrite plus_IZR, Rmult_plus_distr_r, mult_IZR. replace (IZR y * IZR (x / y) * / IZR y)%R with (IZR (x / y)) by now field. apply Zfloor_imp. rewrite plus_IZR. assert (0 <= IZR (x mod y) * / IZR y < 1)%R. assert (forall x' y', (0 < y')%Z -> 0 <= IZR (x' mod y') * / IZR y' < 1)%R. clear. intros x y Hy. split. apply Rmult_le_pos. apply IZR_le. refine (proj1 (Z_mod_lt _ _ _)). now apply Z.lt_gt. apply Rlt_le. apply Rinv_0_lt_compat. now apply IZR_lt. apply Rmult_lt_reg_r with (IZR y). now apply IZR_lt. rewrite Rmult_1_l, Rmult_assoc, Rinv_l, Rmult_1_r. apply IZR_lt. eapply Z_mod_lt. now apply Z.lt_gt. apply Rgt_not_eq. now apply IZR_lt. destruct (Z_lt_le_dec y 0) as [Hy|Hy]. rewrite <- Rmult_opp_opp. rewrite Ropp_inv_permute with (1 := Zy'). rewrite <- 2!opp_IZR. rewrite <- Zmod_opp_opp. apply H. clear -Hy ; lia. apply H. clear -Zy Hy ; lia. split. pattern (IZR (x / y)) at 1 ; rewrite <- Rplus_0_r. apply Rplus_le_compat_l. apply H. apply Rplus_lt_compat_l. apply H. Qed.
imports: Coq(Psatz Reals ZArith) Zaux