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