proposition: Theorem MaxMin : forall (p : float) (r : R), isMax r p -> r <> p :>R -> isMin r (FNPred b radix precision p).
proof: Proof. intros p r H' H'0. rewrite <- (Fopp_Fopp (FNPred b radix precision p)). rewrite <- (Ropp_involutive r). apply MaxOppMin. rewrite FNPredFopFNSucc; auto. rewrite Fopp_Fopp; auto. apply MinMax; auto. apply MaxOppMin; auto. contradict H'0. rewrite <- (Ropp_involutive r); rewrite H'0; auto; unfold FtoRradix in |- *; rewrite Fopp_correct; auto; apply Ropp_involutive. Qed.
imports: Reals ZArith List PeanoNat Psatz