proposition: Theorem RoundedProjector : forall P, RoundedModeP P -> ProjectorP b radix P.
proof: Proof. intros P H'; red in |- *; simpl in |- *. intros p q H'0 H'1. red in H'. elim H'; intros H'2 H'3; elim H'3; intros H'4 H'5; elim H'5; intros H'6 H'7; case (H'6 p q); clear H'5 H'3 H'; auto. intros H'; apply (ProjectMin b radix p); auto. intros H'; apply (ProjectMax b radix p); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz