proposition: Theorem inbetween_shr : forall x m e l n, (0 <= m)%Z -> inbetween_float radix2 m e x l -> let '(mrs, e') := shr (shr_record_of_loc m l) e n in inbetween_float radix2 (shr_m mrs) e' x (loc_of_shr_record mrs).
proof: Proof. intros x m e l n Hm Hl. destruct n as [|n|n]. now destruct l as [|[| |]]. 2: now destruct l as [|[| |]]. unfold shr. rewrite iter_pos_nat. rewrite Zpos_eq_Z_of_nat_o_nat_of_P. induction (nat_of_P n). simpl. rewrite Zplus_0_r. now destruct l as [|[| |]]. rewrite iter_nat_S. rewrite inj_S. unfold Z.succ. rewrite Zplus_assoc. revert IHn0. apply inbetween_shr_1. clear -Hm. induction n0. now destruct l as [|[| |]]. rewrite iter_nat_S. revert IHn0. generalize (iter_nat shr_1 n0 (shr_record_of_loc m l)). clear. intros (m, r, s) Hm. now destruct m as [|[m|m|]|m] ; try (now elim Hm) ; destruct r as [|] ; destruct s as [|]. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative