proposition: Lemma IVT_cor : forall (f:R -> R) (x y:R), continuity f -> x <= y -> f x * f y <= 0 -> { z:R | x <= z <= y /\ f z = 0 }.
proof: Proof. intros. destruct (total_order_T 0 (f x)) as [[Hltx|Heqx]|Hgtx]. 2:{ exists x. split. - split; [ right; reflexivity | assumption ]. - symmetry ; assumption. } 1,2:destruct (total_order_T 0 (f y)) as [[Hlty|Heqy]|Hgty]. - cut (0 < f x * f y); [ intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 H2)) | apply Rmult_lt_0_compat; assumption ]. - exists y. split. + split; [ assumption | right; reflexivity ]. + symmetry ; exact Heqy. - cut (x < y). + intro. assert (H3 := IVT (- f)%F x y (continuity_opp f H) H2). cut ((- f)%F x < 0). * cut (0 < (- f)%F y). -- intros. destruct (H3 H5 H4) as (x0,[]). exists x0. split. ++ assumption. ++ unfold opp_fct in H7. rewrite <- (Ropp_involutive (f x0)). apply Ropp_eq_0_compat; assumption. -- unfold opp_fct; apply Ropp_0_gt_lt_contravar; assumption. * unfold opp_fct. apply Rplus_lt_reg_l with (f x); rewrite Rplus_opp_r; rewrite Rplus_0_r; assumption. + inversion H0. * assumption. * rewrite H2 in Hltx. elim (Rlt_irrefl _ (Rlt_trans _ _ _ Hgty Hltx)). - cut (x < y). + intro. apply IVT; assumption. + inversion H0. * assumption. * rewrite H2 in Hgtx. elim (Rlt_irrefl _ (Rlt_trans _ _ _ Hlty Hgtx)). - exists y. split. + split; [ assumption | right; reflexivity ]. + symmetry ; assumption. - cut (0 < f x * f y). + intro. elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H2 H1)). + rewrite <- Rmult_opp_opp; apply Rmult_lt_0_compat; apply Ropp_0_gt_lt_contravar; assumption. Qed.
imports: Sumbool Rbase Rfunctions SeqSeries Ranalysis1 Lra