proposition: Theorem RoundedModeProjectorIdemEq : forall (P : R -> float -> Prop) (p q : float), RoundedModeP b radix P -> Fbounded b p -> P (FtoR radix p) q -> p = q :>R.
proof: Proof. intros P p q H' H'0 H'1. cut (MinOrMaxP b radix P); [ intros Mn; case (Mn p q); auto; intros Mn1 | apply H']. apply sym_eq; apply MinEq with (1 := Mn1); auto. apply (RoundedModeProjectorIdem (isMin b radix)); auto. apply MinRoundedModeP with (precision := precision); auto. apply sym_eq; apply MaxEq with (1 := Mn1); auto. apply (RoundedModeProjectorIdem (isMax b radix)); auto. apply MaxRoundedModeP with (precision := precision); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz