proposition: Lemma Boundedx2y1_aux: (exists x':float, (FtoRradix x'=x2*y1)%R /\ (Fbounded b x') /\ (Fexp x'=Fexp x2+Fexp y1)%Z ).
proof: Proof. exists (Fmult x2 y1). 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 Fx2; elim Fy1; intros. apply Z.lt_le_trans with (Zpos (vNum bt)*Zpos (vNum b'))%Z; auto with zarith. case (Zle_lt_or_eq 0%Z (Z.abs (Fnum x2))); [auto with zarith| |]. intros I; apply Z.lt_le_trans with (Z.abs (Fnum x2) * Zpos (vNum b'))%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