proposition: Theorem MinMax : forall (p : float) (r : R), isMin r p -> r <> p :>R -> isMax r (FNSucc b radix precision p).
proof: Proof. intros p r H' H'0. split. apply FcanonicBound with (radix := radix); auto with zarith. apply FNSuccCanonic; auto. inversion H'; auto. split. case (Rle_or_lt (FNSucc b radix precision p) r); intros H'2; auto. absurd (FNSucc b radix precision p <= p)%R. apply Rlt_not_le. unfold FtoRradix in |- *; apply FNSuccLt; auto. inversion H'; auto. elim H0; intros H'1 H'3; apply H'3; auto. apply FcanonicBound with (radix := radix); auto with zarith. apply FNSuccCanonic; auto. apply Rlt_le; auto. intros f H'2 H'3. replace (FtoRradix f) with (FtoRradix (Fnormalize radix b precision f)). unfold FtoRradix in |- *; apply FNSuccProp; auto. inversion H'; auto. apply FcanonicBound with (radix := radix); auto with zarith. apply FnormalizeCanonic; easy. apply Rlt_le_trans with r; auto. case (Rle_or_lt r p); auto. intros H'4; contradict H'0. apply Rle_antisym; auto; apply isMin_inv1 with (1 := H'); auto. rewrite FnormalizeCorrect; auto. unfold FtoRradix in |- *; apply FnormalizeCorrect; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz