proposition: Lemma be2MuchSmaller: ~(FtoRradix al2=0)%R -> ~(FtoRradix u2=0)%R -> (MSB radix al2 < LSB radix be2)%Z.
proof: Proof. intros. assert (FtoRradix be2 = (Fminus radix (Fplus radix u1 al1) be1))%R. rewrite be2Def; unfold FtoRradix; rewrite Fminus_correct; auto; rewrite Fplus_correct; auto; ring. rewrite LSB_comp with radix be2 (Fminus radix (Fplus radix u1 al1) be1); auto with zarith. 2: contradict Be2NonZero. 2: unfold FtoRradix; apply is_Fzero_rep1; auto. apply Z.lt_le_trans with (Z.min (LSB radix (Fplus radix u1 al1)) (LSB radix be1)). 2: apply LSBMinus; auto. 2: contradict Be2NonZero. 2: rewrite H1; unfold FtoRradix; apply is_Fzero_rep1; auto. apply Zmin_Zlt. apply Z.lt_le_trans with (Z.min (LSB radix u1 ) (LSB radix al1)). 2: apply LSBPlus; auto. apply Zmin_Zlt. apply Z.le_lt_trans with (MSB radix u2). apply MSB_monotone; auto. contradict H; unfold FtoRradix; apply is_Fzero_rep1; auto. contradict H0; unfold FtoRradix; apply is_Fzero_rep1; auto. repeat rewrite Fabs_correct; auto. apply TwoSumProp with bo y al1; auto. rewrite MSB_comp with radix u2 (Fminus radix (Fmult a x) u1); auto with zarith. apply MSBroundLSB with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. rewrite Fmult_correct; auto with real. contradict H0. apply trans_eq with (FtoRradix (Fminus radix (Fmult a x) u1)). rewrite u2Def; unfold FtoRradix; rewrite Fminus_correct; auto; rewrite Fmult_correct; auto; ring. unfold FtoRradix; apply is_Fzero_rep1; auto. contradict H0; unfold FtoRradix; apply is_Fzero_rep1; auto. fold FtoRradix; rewrite u2Def; unfold FtoRradix; rewrite Fminus_correct; auto; rewrite Fmult_correct; auto; ring. rewrite MSB_comp with radix al2 (Fminus radix (Fplus radix y u2) al1); auto with zarith. apply MSBroundLSB with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. rewrite Fplus_correct; auto with real. contradict H. apply trans_eq with (FtoRradix (Fminus radix (Fplus radix y u2) al1)). rewrite al2Def; unfold FtoRradix; rewrite Fminus_correct; auto; rewrite Fplus_correct; auto; ring. unfold FtoRradix; apply is_Fzero_rep1; auto. contradict H; unfold FtoRradix; apply is_Fzero_rep1; auto. fold FtoRradix; rewrite al2Def; unfold FtoRradix; rewrite Fminus_correct; auto; rewrite Fplus_correct; auto; ring. cut (~(u1+al1=0)%R). intros I; contradict I. unfold FtoRradix; rewrite <- Fplus_correct; auto; apply is_Fzero_rep1; auto. contradict Be2NonZero. rewrite be2Def; rewrite Be2NonZero. assert (FtoRradix be1=0)%R; auto with real. rewrite <- FzeroisReallyZero with radix (-(dExp bo))%Z. unfold FtoRradix; apply sym_eq. apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. apply FboundedFzero. rewrite FzeroisReallyZero; rewrite <- Be2NonZero; auto. apply Zlt_powerRZ with radix; auto with real zarith. apply IZR_le; lia. apply Rle_lt_trans with (FtoR radix (Float (S 0) (MSB radix al2))); [unfold FtoR; simpl; right; ring|idtac]. apply Rle_lt_trans with (FtoR radix (Fabs al2));[apply MSB_le_abs; auto with zarith|idtac]. contradict H; unfold FtoRradix; apply is_Fzero_rep1; auto. rewrite Fabs_correct; auto; fold FtoRradix. apply Rlt_le_trans with (powerRZ radix (Fexp be1)). 2: apply Rle_powerRZ; auto with real zarith. 2: apply IZR_le; lia. 2: apply Fexp_le_LSB; auto. apply Rlt_le_trans with (powerRZ radix (Z.min (Fexp u1) (Fexp al1))). cut (Rabs al2 < powerRZ radix (Fexp u1))%R;[intros I1|idtac]. cut (Rabs al2 < powerRZ radix (Fexp al1))%R;[intros I2|idtac]. unfold Z.min; case (Fexp u1 ?= Fexp al1)%Z; auto with real zarith. rewrite al2Def; apply Rlt_le_trans with (Fulp bo radix p al1). unfold FtoRradix; apply RoundedModeUlp with (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. unfold Fulp; rewrite FcanonicFnormalizeEq; auto with zarith real; left; auto. apply Rle_lt_trans with (Rabs u2). unfold FtoRradix; apply TwoSumProp with bo y al1; auto. rewrite u2Def; apply Rlt_le_trans with (Fulp bo radix p u1). unfold FtoRradix; apply RoundedModeUlp with (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. unfold Fulp; rewrite FcanonicFnormalizeEq; auto with zarith real; left; auto. apply Rle_powerRZ; try apply IZR_le; auto with real zarith. apply Zlt_le_weak. case (Zle_or_lt (Fexp be1) (Z.min (Fexp u1) (Fexp al1))); auto. intros; contradict Be2NonZero. rewrite be2Def. assert (FtoRradix be1=u1+al1)%R; auto with real. unfold FtoRradix; apply plusExact1 with bo p; auto with zarith. elim u1Def; auto. elim al1Def; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz