proposition: Theorem RleMinR0 : forall (r : R) (min : float), (0 <= r)%R -> isMin b radix r min -> (0 <= min)%R.
proof: Proof. intros r min H' H'0. rewrite <- (FzeroisZero radix b). case H'; intros H'1. apply (MonotoneMin b radix) with (p := FtoRradix (Fzero (- dExp b))) (q := r); auto. unfold FtoRradix in |- *; rewrite (FzeroisZero radix b); auto. apply (RoundedModeProjectorIdem (isMin b radix)); auto. apply MinRoundedModeP with (precision := precision); auto with zarith. apply FboundedFzero; auto. replace (FtoR radix (Fzero (- dExp b))) with (FtoRradix min); auto with real. apply sym_eq; apply (ProjectMin b radix). apply FboundedFzero; auto. rewrite <- H'1 in H'0; rewrite <- (FzeroisZero radix b) in H'0; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz