proposition: Lemma Boundedx1y2_aux: (exists x':float, (FtoRradix x'=x1*y2)%R /\ (Fbounded b x') /\ (Fexp x'=Fexp x1+Fexp y2)%Z ).
proof: Proof. exists (Fmult x1 y2). split;[unfold FtoRradix; rewrite Fmult_correct; auto with real zarith|idtac]. split;[idtac|simpl; auto]. unfold Fmult; split; simpl; auto with zarith. rewrite Zabs_Zmult. elim Fx1; elim Fy2; intros. apply Z.lt_le_trans with (Zpos (vNum b')*Zpos (vNum bt))%Z; auto with zarith. case (Zle_lt_or_eq 0%Z (Z.abs (Fnum x1))); [auto with zarith| | ]. intros I; apply Z.lt_le_trans with (Z.abs (Fnum x1) * Zpos (vNum bt))%Z; auto with zarith. apply Zmult_lt_compat_l; auto with zarith. intros I; rewrite <- I; rewrite Zmult_0_l. apply Z.mul_pos_pos; auto with zarith. unfold b'; rewrite p'GivesBound; auto with zarith. rewrite p''GivesBound; auto with zarith. rewrite <- Zpower_nat_is_exp. rewrite pGivesBound; auto with zarith. apply Zpower_nat_monotone_le; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz