proposition: Lemma shr_limit : forall mrs e n, ((0 < shr_m mrs)%Z \/ shr_m mrs = 0%Z /\ (shr_r mrs || shr_s mrs = true)%bool) -> (shr_m mrs < radix2 ^ (n - 1))%Z -> fst (shr mrs e n) = {| shr_m := 0%Z; shr_r := false; shr_s := true |}.
proof: Proof. intros mrs e n Hmrs0. set (n' := (n - 1)%Z). replace n with (n' + 1)%Z; [| lia]. destruct n' as [| p | p ]. - simpl. destruct Hmrs0 as [Hmrs0 | Hmrs0]; [lia | intros _]. destruct mrs as [m r s]. simpl in Hmrs0. destruct Hmrs0 as [Hmrs00 Hmrs01]. rewrite Hmrs00. simpl. now rewrite Hmrs01. - intros Hmrs1. rewrite !Z.add_1_r. rewrite <-Pos2Z.inj_succ. simpl shr. rewrite iter_pos_nat. rewrite Pos2Nat.inj_succ. simpl iter_nat. rewrite <-(positive_nat_Z p) in Hmrs1. rewrite <-(Pos2Nat.id p) at 2. revert Hmrs1. revert Hmrs0. revert mrs. induction (nat_of_P p) as [| n'' IHn'']. + simpl in *. intros mrs [Hmrs0 | [Hmrs00 Hmrs01]] Hmrs1; [lia |]. destruct mrs as [m r s]. simpl in Hmrs00, Hmrs01, Hmrs1. rewrite Hmrs00. simpl. now rewrite Hmrs01. + intros mrs Hmrs0 Hmrs1. simpl iter_nat. destruct (le_shr1_le mrs) as [[Hmrs'0 Hmrs'1] Hmrs'2]; [destruct Hmrs0; lia |]. set (mrs' := shr_1 mrs). apply IHn''. * case (0 <? shr_m (shr_1 mrs))%Z eqn:Hmrs'3; [apply Zlt_is_lt_bool in Hmrs'3; now left |]. fold mrs' in Hmrs'0, Hmrs'1, Hmrs'2, Hmrs'3. apply Z.ltb_ge in Hmrs'3. apply Z.mul_nonneg_cancel_l in Hmrs'0; [| easy]. apply (Z.le_antisymm _ _ Hmrs'3) in Hmrs'0. right. split; [assumption |]. destruct Hmrs0 as [Hmrs0 | [Hmrs00 Hmrs01]]. -- rewrite Hmrs'0 in Hmrs'2. simpl in Hmrs'2. assert (Hmrs2 : shr_m mrs = 1%Z) by lia. destruct mrs as [m r s]. simpl in Hmrs2. unfold mrs'. now rewrite Hmrs2. -- destruct mrs as [m r s]. simpl in Hmrs00, Hmrs01. unfold mrs'. now rewrite Hmrs00. * simpl Z.of_nat in Hmrs1. unfold mrs'. rewrite Zpos_P_of_succ_nat in Hmrs1. rewrite Z.pow_succ_r in Hmrs1; [| lia]. apply (Z.le_lt_trans _ _ _ Hmrs'1) in Hmrs1. apply Z.mul_lt_mono_pos_l in Hmrs1; [assumption | easy]. - simpl. destruct Hmrs0 as [Hmrs0 | Hmrs0]; lia. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative