proposition: Theorem FboundedEqExp : forall (b : Fbound) (p q : float), Fbounded b p -> p = q :>R -> (Fexp p <= Fexp q)%R -> Fbounded b q.
proof: Proof. intros b p q H' H'0 H'1; split. apply Z.le_lt_trans with (Z.abs (Fnum p)); [ idtac | try apply H' ]. apply Z.le_trans with (Z.abs (Fnum (Fshift radix (Z.abs_nat (Fexp q - Fexp p)) q))); auto. unfold Fshift in |- *; simpl in |- *; auto. rewrite Zabs_Zmult. pattern (Z.abs (Fnum q)) at 1 in |- *; replace (Z.abs (Fnum q)) with (Z.abs (Fnum q) * 1)%Z; [ apply Zle_Zmult_comp_l | lia ]; auto with zarith. rewrite Z.abs_eq; simpl in |- *; auto with zarith. apply Zpower_NR1; lia. apply Zpower_NR0; lia. cut (Fexp p <= Fexp q)%Z; [ intros E2 | idtac ]. apply le_IZR; auto. apply (Rle_monotony_contra_exp radix) with (z := Fexp p); auto with real arith. pattern (Fexp p) at 2 in |- *; replace (Fexp p) with (Fexp (Fshift radix (Z.abs_nat (Fexp q - Fexp p)) q)); auto. rewrite <- (fun x => Rabs_pos_eq (powerRZ radix x)); auto with real zarith. rewrite <- Rabs_Zabs. rewrite <- Rabs_mult. change (Rabs (FtoRradix (Fshift radix (Z.abs_nat (Fexp q - Fexp p)) q)) <= Z.abs (Fnum p) * powerRZ radix (Fexp p))%R in |- *. unfold FtoRradix in |- *; rewrite FshiftCorrect; auto. fold FtoRradix in |- *; rewrite <- H'0. rewrite <- (Fabs_correct radix); auto with real zarith. now apply powerRZ_le, IZR_lt. unfold Fshift in |- *; simpl in |- *. rewrite inj_abs; [ ring | auto with zarith ]. now apply le_IZR. cut (Fexp p <= Fexp q)%Z; [ intros E2 | apply le_IZR ]; auto. apply Z.le_trans with (Fexp p); try apply H'; now apply le_IZR. Qed.
imports: Reals ZArith List PeanoNat Psatz