proposition: Lemma le_choice_mode_le : forall m sx mx lx, (mx <= choice_mode m sx mx lx <= mx + 1)%Z.
proof: Proof. unfold choice_mode; intros m sx mx lx; case m; simpl; try lia; apply le_cond_incr_le. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative