proposition: Lemma le_shr1_le : forall mrs, (0 <= shr_m mrs)%Z -> (0 <= 2 * shr_m (shr_1 mrs) <= shr_m mrs)%Z /\ (shr_m mrs < 2 * (shr_m (shr_1 mrs) + 1))%Z.
proof: Proof. destruct mrs as [m r s]. simpl. destruct m as [| p | p]; [simpl; lia | intros _ | intros; easy]. destruct p; simpl; [| | lia]. - rewrite Pos2Z.inj_xO, Pos2Z.inj_xI. lia. - rewrite Pos2Z.inj_xO. lia. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative