proposition: Lemma continuity_ab_min : forall (f:R -> R) (a b:R), a <= b -> (forall c:R, a <= c <= b -> continuity_pt f c) -> exists mx : R, (forall c:R, a <= c <= b -> f mx <= f c) /\ a <= mx <= b.
proof: Proof. intros. cut (forall c:R, a <= c <= b -> continuity_pt (- f0) c). - intro; assert (H2 := continuity_ab_maj (- f0)%F a b H H1); elim H2; intros x0 H3; exists x0; intros; split. + intros; rewrite <- (Ropp_involutive (f0 x0)); rewrite <- (Ropp_involutive (f0 c)); apply Ropp_le_contravar; elim H3; intros; unfold opp_fct in H5; apply H5; apply H4. + elim H3; intros; assumption. - intros. assert (H2 := H0 _ H1). apply (continuity_pt_opp _ _ H2). Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type