proposition: Theorem RoundedModeBounded : forall P (r : R) (q : float), RoundedModeP b radix P -> P r q -> Fbounded b q.
proof: Proof. intros P r q H' H'0. case H'. intros H'1 H'2; elim H'2; intros H'3 H'4; elim H'4; intros H'5 H'6; case H'5 with (1 := H'0); clear H'4 H'2; intros H; case H; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz