proposition: Theorem RoundedModeProjectorIdem : forall P (p : float), RoundedModeP b radix P -> Fbounded b p -> P p p.
proof: Proof. intros P p H' H. elim H'; intros H'0 H'1; elim H'1; intros H'2 H'3; elim H'3; intros H'4 H'5; clear H'3 H'1. case (H'0 p). intros x H'6. apply (H'2 p p x); auto. apply sym_eq; apply (RoundedProjector _ _ P H'); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz