proposition: Theorem FboundedShiftLess : forall (b : Fbound) (f : float) (n m : nat), m <= n -> Fbounded b (Fshift radix n f) -> Fbounded b (Fshift radix m f).
proof: Proof. intros b f n m H' H'0; split; auto. simpl in |- *; auto. apply Z.le_lt_trans with (Z.abs (Fnum (Fshift radix n f))). simpl in |- *; replace m with (m + 0); auto with arith. replace n with (m + (n - m)); auto with arith. repeat rewrite Zpower_nat_is_exp. repeat rewrite Zabs_Zmult; auto. apply Zle_Zmult_comp_l; auto with zarith. apply Zle_Zmult_comp_l; auto with zarith. rewrite 2!Z.abs_eq by (apply Zpower_NR0; lia). apply Zpower_nat_monotone_le; lia. apply H'0. apply Z.le_trans with (Fexp (Fshift radix n f)); try apply H'0. simpl in |- *; unfold Zminus in |- *; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz