proposition: Theorem RleBoundRoundl : forall P, RoundedModeP b radix P -> forall (p q : float) (r : R), Fbounded b p -> (p <= r)%R -> P r q -> (p <= q)%R.
proof: Proof. intros P H' p q r H'0 H'1 H'2; case H'1; intros H'3. cut (MonotoneP radix P); [ intros Mn | apply RoundedModeP_inv4 with (1 := H'); auto ]. apply (Mn p r); auto. apply RoundedModeProjectorIdem with (P := P); auto. rewrite RoundedModeProjectorIdemEq with (P := P) (p := p) (q := q); auto with real. cut (CompatibleP b radix P); [ intros Cp | apply RoundedModeP_inv2 with (1 := H'); auto ]. apply (Cp r p q); auto. apply RoundedModeBounded with (P := P) (r := r); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz