proposition: Theorem RleRoundedLessR0 : forall (P : R -> float -> Prop) (p : float) (r : R), RoundedModeP b radix P -> P r p -> (r <= 0)%R -> (p <= 0)%R.
proof: Proof. intros P p r H' H'0 H'1. case H'. intros H'2 H'3; Elimc H'3; intros H'3 H'4; Elimc H'4; intros H'4 H'5; case (H'4 r p); auto; intros H'6. apply Rle_trans with r; auto; apply isMin_inv1 with (1 := H'6). apply RleMaxR0 with (r := r); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz