proposition: Lemma Boundedx1y1: (exists x':float, (FtoRradix x'=x1*y1)%R /\ (Fbounded b x')).
proof: Proof. elim Boundedx1y1_aux; intros f T; elim T ; intros T1 T2; elim T2; intros. exists f; split; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz