proposition: Theorem format_REM_ZR: forall x y : R, format x -> format y -> format (x - IZR (Ztrunc (x/y)) * y).
proof: Proof. Proof with auto with typeclass_instances. intros x y Fx Fy. apply format_REM; try easy... intros K. apply Z.abs_0_iff. rewrite <- Ztrunc_abs. rewrite Ztrunc_floor by apply Rabs_pos. apply Zle_antisym. replace 0%Z with (Zfloor (/2)). apply Zfloor_le. now apply Rlt_le. apply Zfloor_imp. simpl ; lra. apply Zfloor_lub. apply Rabs_pos. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative Sterbenz Mult_error