proposition: Theorem RleMaxR0 : forall (r : R) (max : float), (r <= 0)%R -> isMax b radix r max -> (max <= 0)%R.
proof: Proof. intros r max H' H'0. rewrite <- (FzeroisZero radix b). case H'; intros H'1. apply (MonotoneMax b radix) with (q := FtoRradix (Fzero (- dExp b))) (p := r); auto. unfold FtoRradix in |- *; rewrite FzeroisZero; auto. apply (RoundedModeProjectorIdem (isMax b radix)); auto. apply MaxRoundedModeP with (precision := precision); auto. apply FboundedFzero; auto. replace (FtoR radix (Fzero (- dExp b))) with (FtoRradix max); auto with real. apply sym_eq; apply (ProjectMax 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