proposition: Theorem inbetween_float_new_location_single : forall x m e l, inbetween_float m e x l -> inbetween_float (Z.div m beta) (e + 1) x (new_location beta (Zmod m beta) l).
proof: Proof. intros x m e l Hx. replace (radix_val beta) with (Zpower beta 1). now apply inbetween_float_new_location. apply Zmult_1_r. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop