proposition: Lemma IVT_seq_lemma : forall (xy : IR ** IR) (x:=fstT xy) (y:=sndT xy) (Hxy : (I x) ** (I y)) (Hx := fstT Hxy) (Hy := sndT Hxy), x [<] y -> F x (incF _ Hx) [<=] z /\ z [<=] F y (incF _ Hy) -> {xy0 : IR ** IR | let x0 := fstT xy0 in let y0 := sndT xy0 in {Hxy0 : (I x0) ** (I y0) | x0 [<] y0 | let Hx0 := fstT Hxy0 in let Hy0 := sndT Hxy0 in F x0 (incF _ Hx0) [<=] z /\ z [<=] F y0 (incF _ Hy0) /\ y0[-]x0 [=] Two [/]ThreeNZ[*] (y[-]x) /\ x [<=] x0 /\ y0 [<=] y}}.
proof: Proof. intros xy x y Hxy Hx Hy H H0. set (x1 := (Two[*]x[+]y) [/]ThreeNZ) in *. set (y1 := (x[+]Two[*]y) [/]ThreeNZ) in *. assert (H1 : x1 [<] y1). unfold x1, y1 in |- *; apply lft_rht; auto. cut (I x1). intro H2. cut (I y1). intro H3. cut (F x1 (incF _ H2) [<] F y1 (incF _ H3)); [ intro H4 | auto ]. elim (less_cotransitive_unfolded _ _ _ H4 z); intros. exists (pairT x1 y); exists (pairT H2 Hy); simpl in |- *; repeat split; auto. apply less_leEq_trans with y1. auto. apply less_leEq; unfold x1, y1 in |- *; apply rht_b; auto. apply less_leEq; auto. elim H0; auto. unfold x1 in |- *; apply smaller_rht. unfold x1 in |- *; apply less_leEq; apply a_lft; auto. apply leEq_reflexive. exists (pairT x y1); exists (pairT Hx H3); simpl in |- *; repeat split; auto. apply leEq_less_trans with x1. apply less_leEq; unfold x1, y1 in |- *; apply a_lft; auto. auto. elim H0; auto. apply less_leEq; auto. unfold y1 in |- *; apply smaller_lft; auto. apply leEq_reflexive. apply less_leEq; unfold y1 in |- *; apply rht_b; auto. unfold y1 in |- *; inversion_clear Hx; inversion_clear Hy; split. apply leEq_transitive with x; auto. apply less_leEq; apply less_transitive_unfolded with x1; unfold x1 in |- *; [ apply a_lft | apply lft_rht ]; auto. apply leEq_transitive with y; auto. apply less_leEq; apply rht_b; auto. unfold x1 in |- *; inversion_clear Hx; inversion_clear Hy; split. apply leEq_transitive with x; auto. apply less_leEq; apply a_lft; auto. apply leEq_transitive with y; auto. apply less_leEq; apply less_transitive_unfolded with y1; unfold y1 in |- *; [ apply lft_rht | apply rht_b ]; auto. Qed.
imports: CoRN.ftc.Continuity