proposition: Theorem MinOrMax_Fopp : forall (x : R) (f : float), MinOrMax (- x) (Fopp f) -> MinOrMax x f.
proof: Proof. unfold MinOrMax in |- *; intros x f H. rewrite <- (Ropp_involutive x); rewrite <- (Fopp_Fopp f). case H; intros H1. right; apply MinOppMax; auto. left; apply MaxOppMin; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz