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