proposition: Theorem format_REM_N : forall choice, forall x y : R, format x -> format y -> format (x - IZR (Znearest choice (x/y)) * y).
proof: Proof. Proof with auto with typeclass_instances. intros choice x y Fx Fy. apply format_REM; try easy... intros K. apply Znearest_imp. now rewrite Rminus_0_r. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative Sterbenz Mult_error