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 and z [<] F y (incF _ Hy) -> {xy0 : IR ** IR | let x0 := fstT xy0 in let y0 := sndT xy0 in {Hxy0 : (I x0) ** (I y0) | let Hx0 := fstT Hxy0 in let Hy0 := sndT Hxy0 in x0 [<] y0 and F x0 (incF _ Hx0) [<] z and z [<] F y0 (incF _ Hy0) | y0[-]x0 [=] Two [/]ThreeNZ[*] (y[-]x) /\ x [<=] x0 /\ y0 [<=] y}}.
proof: Proof. do 6 intro. intros H H0. set (x1 := (Two[*]x[+]y) [/]ThreeNZ) in *. set (y1 := (x[+]Two[*]y) [/]ThreeNZ) in *. cut (x1 [<] y1). intro H1. 2: 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_transitive_unfolded with y1; unfold x1, y1 in |- *; [ apply lft_rht | apply rht_b ]; auto. 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 less_transitive_unfolded with x1; unfold x1, y1 in |- *; [ apply a_lft | apply lft_rht ]; auto. elim H0; 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.WeakIVT CoRN.ftc.CalculusTheorems