proposition: Theorem MaxOppMin : forall (p : float) (r : R), isMax r p -> isMin (- r) (Fopp p).
proof: Proof. intros p r H'; split. apply oppBounded; case H'; auto. split. unfold FtoRradix in |- *; rewrite Fopp_correct. apply Ropp_le_contravar; apply isMax_inv1 with (1 := H'); auto. intros f H'0 H'1. rewrite <- (Fopp_Fopp f). unfold FtoRradix in |- *; repeat rewrite Fopp_correct. apply Ropp_le_contravar. rewrite <- (Fopp_correct radix f). elim H'. intros H'2 H'3; elim H'3; intros H'4 H'5; apply H'5; clear H'3. apply oppBounded; auto. rewrite <- (Ropp_involutive r). unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz