proposition: Lemma le_shr_le : forall mrs e n, (0 <= shr_m mrs)%Z -> (0 <= n)%Z -> (0 <= 2 ^ n * shr_m (fst (shr mrs e n)) <= shr_m mrs)%Z /\ (shr_m mrs < 2 ^ n * (shr_m (fst (shr mrs e n)) + 1))%Z.
proof: Proof. intros mrs e n Hmrs. destruct n as [| n | n ]; [intros _; simpl; now destruct (shr_m mrs); simpl; lia | intro Hn | lia]. unfold shr. rewrite iter_pos_nat. rewrite <-!(positive_nat_Z n). simpl fst. induction (nat_of_P n) as [| n' IHn']; [simpl; destruct (shr_m mrs); simpl; lia |]. rewrite !Nat2Z.inj_succ. rewrite Z.pow_succ_r; [| apply Zle_0_nat]. rewrite iter_nat_S. rewrite (Z.mul_comm 2%Z _), <-Z.mul_assoc. destruct IHn' as [[IHn'1 IHn'2] IHn'3]. apply Z.mul_nonneg_cancel_l in IHn'1; [| lia]. repeat split; [| transitivity (2 ^ Z.of_nat n' * shr_m (iter_nat shr_1 n' mrs))%Z; [| auto] |]. - apply Z.mul_nonneg_nonneg; [lia |]. now apply le_shr1_le. - apply Z.mul_le_mono_nonneg_l; [lia |]. now apply le_shr1_le. - apply Z.lt_le_trans with (2 ^ Z.of_nat n' * (shr_m (iter_nat shr_1 n' mrs) + 1))%Z; [assumption |]. rewrite <-Z.mul_assoc. apply Z.mul_le_mono_nonneg_l; [lia |]. apply Ztac.Zlt_le_add_1. now apply le_shr1_le. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative