proposition: Lemma cousin : forall a b delta, ~ ~ exists ptd, pointed_subdiv ptd /\ fine delta ptd /\ SF_h ptd = Rmin a b /\ last (SF_h ptd) (SF_lx ptd) = Rmax a b.
proof: Proof. intros a b delta H. assert (forall ptd, ~ (pointed_subdiv ptd /\ fine delta ptd /\ SF_h ptd = Rmin a b /\ last (SF_h ptd) (SF_lx ptd) = Rmax a b)) as Hdelta. intros ptd Hptd. apply H ; now exists ptd. clear H. set (M := fun y => Rmin a b <= y <= Rmax a b /\ exists ptd, (pointed_subdiv ptd /\ fine delta ptd /\ SF_h ptd = Rmin a b /\ last (SF_h ptd) (SF_lx ptd) = y)). assert (exists b', is_lub M b') as Hb'. apply completeness_weak. exists (Rmax a b). intros y Hy. apply Hy. exists (Rmin a b). split. split. apply Rle_refl. apply Rmin_Rmax. exists (SF_nil (Rmin a b)). simpl. split. intros i Hi. apply Nat.nlt_0_r in Hi ; destruct Hi. split. intros i Hi. apply Nat.nlt_0_r in Hi ; destruct Hi. split ; easy. destruct Hb' as (b', H). assert (forall e : posreal, ~ ~ (exists y, M y /\ b' - e < y)) as H1. now apply lub_cara. apply (H1 (delta b')). intro H2. destruct H2 as (y, H2). clear H1. destruct H2 as (H2, H1). assert (M y) as Hy. assumption. destruct H2 as (H3, H2). destruct H2 as (s, H2). destruct H2 as (H2,H4). destruct H4 as (H4, H0). destruct H0 as (H5, H0). set (s' := SF_rcons s (b',b')). assert (pointed_subdiv s' /\ SF_h s' = Rmin a b /\ last (SF_h s') (SF_lx s') = b') as HH. split. unfold pointed_subdiv ; unfold s'. intros i Hi. rewrite SF_size_rcons in Hi. apply ->Nat.lt_succ_r in Hi. case (eq_nat_dec i (SF_size s)) => His. rewrite His. replace (nth 0 (SF_lx (SF_rcons s (b', b'))) (SF_size s)) with (last (SF_h s) (SF_lx s)). replace (nth 0 (SF_ly (SF_rcons s (b', b'))) (SF_size s)) with b'. replace (nth 0 (SF_lx (SF_rcons s (b', b'))) (S (SF_size s))) with b'. split. rewrite H0. unfold is_lub in H. apply H. apply Hy. apply Rle_refl. rewrite SF_lx_rcons. simpl fst. replace (S (SF_size s)) with (Peano.pred (size (rcons (SF_lx s) b')) ). rewrite nth_last. rewrite last_rcons. easy. rewrite size_rcons. rewrite <- SF_size_lx. simpl ; easy. rewrite SF_ly_rcons. simpl snd. replace (SF_size s) with (Peano.pred (size (rcons (SF_ly s) b'))). rewrite nth_last. rewrite last_rcons. easy. rewrite size_rcons. simpl. apply SF_size_ly. rewrite <- nth_last. rewrite SF_size_lx. simpl. rewrite SF_lx_rcons. simpl fst. rewrite nth_rcons. case Hleq : ssrnat.leq. assert (Peano.pred(size (SF_lx s)) = size (SF_t s)) as Hlxsize. rewrite SF_size_lx. simpl ; unfold SF_size ; simpl ; easy. unfold SF_size. rewrite <- Hlxsize. rewrite nth_last. rewrite nth_last. unfold SF_lx. rewrite last_cons. rewrite last_cons. easy. rewrite SF_size_lx in Hleq. by rewrite ssrnat.leqnn in Hleq. rewrite SF_lx_rcons. rewrite SF_ly_rcons. simpl fst. simpl snd. assert (i < SF_size s)%nat as Hsi. apply le_lt_eq_dec in Hi. now destruct Hi. split ; rewrite nth_rcons ; case Hcase : ssrnat.leq ; rewrite nth_rcons ; case Hcase2 : ssrnat.leq. now apply (H2 i). case Hcase3 : eqtype.eq_op. apply Rle_trans with (last (SF_h s) (SF_lx s)). replace (last (SF_h s) (SF_lx s)) with (last 0 (SF_lx s)). apply sorted_last. apply ptd_sort. apply H2. rewrite SF_size_lx. unfold lt. apply le_n_S. apply Hi. case Hs : (SF_lx s). assert (size (SF_lx s) = 0%nat) as Hss. rewrite Hs ; simpl ; easy. rewrite SF_size_lx in Hss. apply MyNat.neq_succ_0 in Hss ; destruct Hss. rewrite last_cons ; rewrite last_cons ; easy. rewrite H0. destruct H as (H, H'). now apply H. move :Hcase2 => /ssrnat.leP Hcase2. apply not_le in Hcase2 ; unfold gt in Hcase2. rewrite SF_size_ly in Hcase2. unfold lt in Hcase2. apply le_S_n in Hcase2. unfold lt in Hsi. assert (S i <= i)%nat as Hcase4. now apply Nat.le_trans with (SF_size s). apply Nat.nle_succ_diag_l in Hcase4 ; destruct Hcase4. move :Hcase => /ssrnat.leP Hcase. rewrite SF_size_lx in Hcase. apply le_n_S in Hi. contradiction. move :Hcase => /ssrnat.leP Hcase. rewrite SF_size_lx in Hcase. apply le_n_S in Hi. contradiction. now apply (H2 i). move :Hcase2 => /ssrnat.leP Hcase2. rewrite SF_size_lx in Hcase2. unfold lt in Hsi. apply le_n_S in Hsi. contradiction. move :Hcase => /ssrnat.leP Hcase. rewrite SF_size_ly in Hcase. unfold lt in Hsi. contradiction. move :Hcase => /ssrnat.leP Hcase. rewrite SF_size_ly in Hcase. unfold lt in Hsi. contradiction. unfold s'. split. unfold SF_rcons. simpl. apply H5. rewrite SF_lx_rcons. rewrite last_rcons. easy. apply (Hdelta s'). split. apply HH. split. unfold fine, s'. rewrite SF_size_rcons. unfold lt. intros i Hi. apply le_S_n in Hi. case (le_lt_eq_dec i (SF_size s)). assumption. intro Hi2. unfold ith_step. replace (nth 0 (SF_lx (SF_rcons s (b', b'))) (S i)) with (nth 0 (SF_lx s) (S i)). replace (nth 0 (SF_lx (SF_rcons s (b', b'))) i) with (nth 0 (SF_lx s) i). replace (nth 0 (SF_ly (SF_rcons s (b', b'))) i) with (nth 0 (SF_ly s) i). now apply (H4 i). rewrite SF_ly_rcons. simpl. rewrite nth_rcons. case Hcase : ssrnat.leq. easy. move :Hcase => /ssrnat.leP Hcase. rewrite SF_size_ly in Hcase. contradiction. rewrite SF_lx_rcons. rewrite nth_rcons. case Hcase : ssrnat.leq. easy. move :Hcase => /ssrnat.leP Hcase. rewrite SF_size_lx in Hcase. apply le_n_S in Hi. contradiction. rewrite SF_lx_rcons. rewrite nth_rcons. case Hcase : ssrnat.leq. easy. move :Hcase => /ssrnat.leP Hcase. rewrite SF_size_lx in Hcase. apply le_n_S in Hi2. contradiction. clear Hi ; intro Hi. rewrite Hi. unfold ith_step. rewrite SF_lx_rcons. rewrite SF_ly_rcons. replace (nth 0 (rcons (SF_lx s) (fst (b', b'))) (S (SF_size s))) with (last 0 (rcons (SF_lx s) (fst (b', b')))). replace (nth 0 (rcons (SF_lx s) (fst (b', b'))) (SF_size s)) with y. replace (nth 0 (rcons (SF_ly s) (snd (b', b'))) (SF_size s)) with (last 0 (rcons (SF_ly s) (snd (b', b')))). rewrite last_rcons ; rewrite last_rcons ; simpl. apply Rplus_lt_reg_l with y. rewrite Rplus_comm. rewrite Rplus_assoc. rewrite Rplus_opp_l. rewrite Rplus_0_r. apply Rplus_lt_reg_l with (- delta b'). rewrite Rplus_comm. replace (- delta b' + (y + delta b')) with y. assumption. rewrite Rplus_comm ; rewrite Rplus_assoc ; rewrite Rplus_opp_r ; rewrite Rplus_0_r ; easy. replace (SF_size s) with (Peano.pred (size (rcons (SF_ly s) (snd (b', b'))))). rewrite nth_last ; easy. rewrite size_rcons. simpl ; rewrite SF_size_ly ; easy. rewrite nth_rcons. rewrite SF_size_lx. case Hcase : ssrnat.leq. rewrite <- H0. replace (SF_size s) with (Peano.pred (size (SF_lx s))). rewrite nth_last. case Hs : (SF_lx s). assert (size (SF_lx s) = S (SF_size s)) as Hss. apply SF_size_lx. rewrite Hs in Hss. unfold size in Hss. apply O_S in Hss ; destruct Hss. rewrite last_cons ; rewrite last_cons ; easy. rewrite SF_size_lx ; simpl ; easy. move :Hcase => /ssrnat.leP Hcase. absurd (S (SF_size s) <= S (SF_size s))%nat. assumption. apply Nat.le_refl. replace (S (SF_size s)) with (Peano.pred (size (rcons (SF_lx s) (fst (b', b'))))). rewrite nth_last ; easy. rewrite size_rcons ; rewrite SF_size_lx ; simpl ; easy. destruct HH as (HH1, HH) ; split. apply HH. replace (Rmax a b) with b'. apply HH. assert ({b' < Rmax a b} + {b' = Rmax a b} + {b' > Rmax a b}) as Hb'. apply total_order_T. destruct Hb' as [Hb'1 | Hb'2]. destruct Hb'1 as [Hb'1 | Hb'3]. set (e:= Rmin ((Rmax a b) - b') ((delta b')/2) ). assert (0 < e) as He. apply Rmin_pos. now apply Rlt_Rminus. apply Rmult_lt_0_compat. apply (cond_pos (delta b')). apply Rinv_0_lt_compat. apply (Rlt_R0_R2). assert (e <= (delta b')/2) as Hed. apply Rmin_r. assert (e <= (Rmax a b) - b') as Hebb'. apply Rmin_l. assert (M (b' + e)) as H42. unfold M. split. split. apply Rle_trans with b'. apply Rle_trans with y. apply H3. now apply H. apply Rplus_le_reg_l with (- b'). rewrite Rplus_opp_l. rewrite <- Rplus_assoc. rewrite Rplus_opp_l. rewrite Rplus_0_l. now apply Rlt_le. apply Rplus_le_reg_l with (- b'). rewrite <- Rplus_assoc. rewrite Rplus_opp_l. rewrite Rplus_0_l. rewrite Rplus_comm. assumption. exists (SF_rcons s' (b'+e, b')). split. unfold pointed_subdiv. rewrite SF_size_rcons ; rewrite SF_lx_rcons ; rewrite SF_ly_rcons. intros i Hi. case (le_lt_eq_dec i (SF_size s')). apply le_S_n ; apply Hi. intro Hi2. replace (nth 0 (rcons (SF_lx s') (fst (b' + e, b'))) i) with (nth 0 (SF_lx s') i). replace (nth 0 (rcons (SF_ly s') (snd (b' + e, b'))) i) with (nth 0 (SF_ly s') i). replace (nth 0 (rcons (SF_lx s') (fst (b' + e, b'))) (S i)) with (nth 0 (SF_lx s') (S i)). now apply (HH1 i). rewrite nth_rcons. rewrite SF_size_lx. rewrite ssrnat.ltnS. by move /ssrnat.ltP :Hi2 => ->. rewrite nth_rcons. rewrite SF_size_ly. by move /ssrnat.ltP :Hi2 => ->. rewrite nth_rcons. rewrite SF_size_lx. by move /ssrnat.ltP :Hi => ->. intro Hi2. rewrite Hi2. replace (nth 0 (rcons (SF_lx s') (fst (b' + e, b'))) (SF_size s')) with b'. replace (nth 0 (rcons (SF_ly s') (snd (b' + e, b'))) (SF_size s')) with (nth 0 (rcons (SF_ly s') (snd (b' + e, b'))) (Peano.pred (size (rcons (SF_ly s') (snd (b' + e, b')))))). replace (nth 0 (rcons (SF_lx s') (fst (b' + e, b'))) (S (SF_size s'))) with (nth 0 (rcons (SF_lx s') (fst (b' + e, b'))) (Peano.pred (size (rcons (SF_lx s') (fst (b' + e, b')))))). rewrite nth_last. rewrite nth_last. rewrite last_rcons. rewrite last_rcons. simpl. split. apply Rle_refl. rewrite <- (Rplus_0_r b') at 1. apply Rplus_le_compat_l. now apply Rlt_le. rewrite size_rcons ; rewrite SF_size_lx ; simpl ; easy. rewrite size_rcons ; rewrite SF_size_ly ; simpl ; easy. rewrite nth_rcons. rewrite SF_size_lx. rewrite ssrnat.leqnn. unfold s'. rewrite SF_lx_rcons ; rewrite SF_size_rcons. rewrite -SF_size_lx. rewrite nth_rcons. rewrite ssrnat.ltnn. by rewrite eqtype.eq_refl. split. intro i. rewrite SF_size_rcons. intro Hi. case (le_lt_eq_dec i (SF_size s')). apply le_S_n. apply Hi. intro Hi2. replace (ith_step (SF_rcons s' (b' + e, b')) i) with (ith_step s' i). replace (nth 0 (SF_ly (SF_rcons s' (b' + e, b'))) i) with (nth 0 (SF_ly s') i). unfold s'. case (le_lt_eq_dec i (SF_size s)). unfold s' in Hi2 ; rewrite SF_size_rcons in Hi2. now apply le_S_n. intro Hi3. replace (ith_step (SF_rcons s (b', b')) i) with (ith_step s i). replace (nth 0 (SF_ly (SF_rcons s (b', b'))) i) with (nth 0 (SF_ly s) i). now apply (H4 i). rewrite SF_ly_rcons ; rewrite nth_rcons. rewrite SF_size_ly. by move /ssrnat.ltP :Hi3 => ->. unfold ith_step. rewrite SF_lx_rcons. rewrite 2!nth_rcons. rewrite SF_size_lx. rewrite ssrnat.ltnS. move /ssrnat.ltP :(Hi3) => ->. rewrite ssrnat.ltnS. apply Nat.lt_le_incl in Hi3. by move /ssrnat.leP :Hi3 => ->. intro Hi3. rewrite Hi3. unfold ith_step. rewrite SF_lx_rcons. replace (nth 0 (rcons (SF_lx s) (fst (b', b'))) (S (SF_size s))) with b'. replace (nth 0 (rcons (SF_lx s) (fst (b', b'))) (SF_size s)) with y. replace (nth 0 (SF_ly (SF_rcons s (b', b'))) (SF_size s)) with b'. apply Rplus_lt_reg_l with (y - delta b'). replace (y - delta b' + (b' - y)) with (b' - delta b') by ring. now replace (y - delta b' + delta b') with y by ring. rewrite SF_ly_rcons. replace (SF_size s) with (Peano.pred (size (rcons (SF_ly s) (snd (b', b'))))). rewrite nth_last. rewrite last_rcons. easy. rewrite size_rcons. simpl. apply SF_size_ly. rewrite nth_rcons. rewrite <- H0. rewrite <- nth_last. rewrite SF_size_lx. rewrite ssrnat.leqnn. simpl. apply set_nth_default. rewrite SF_size_lx. apply ssrnat.leqnn. replace (S (SF_size s)) with (Peano.pred (size (rcons (SF_lx s) (fst (b', b'))))). rewrite nth_last. rewrite last_rcons. easy. rewrite size_rcons ; rewrite SF_size_lx ; simpl ; easy. unfold s'. rewrite SF_ly_rcons. rewrite SF_ly_rcons. rewrite SF_ly_rcons. case (le_lt_eq_dec i (SF_size s)). unfold s' in Hi2 ; rewrite SF_size_rcons in Hi2 ; apply le_S_n ; apply Hi2. intro Hi3. rewrite nth_rcons ; rewrite nth_rcons ; rewrite nth_rcons. rewrite SF_size_ly. move /ssrnat.ltP :(Hi3) => ->. rewrite size_rcons. rewrite ssrnat.ltnS. rewrite SF_size_ly. apply Nat.lt_le_incl in Hi3. by move /ssrnat.leP :Hi3 => ->. intro Hi3 ; rewrite Hi3. replace (nth 0 (rcons (SF_ly s) (snd (b', b'))) (SF_size s)) with b'. rewrite nth_rcons. rewrite size_rcons. rewrite SF_size_ly. rewrite ssrnat.leqnn. replace (SF_size s) with (Peano.pred (size (rcons (SF_ly s) (snd (b', b'))))). rewrite nth_last. rewrite last_rcons ; easy. rewrite size_rcons ; rewrite SF_size_ly ; simpl ; easy. rewrite nth_rcons. rewrite SF_size_ly. rewrite ssrnat.ltnn. by rewrite eqtype.eq_refl. unfold ith_step. rewrite SF_lx_rcons. rewrite nth_rcons ; rewrite nth_rcons. rewrite SF_size_lx. rewrite ssrnat.ltnS. move /ssrnat.ltP :(Hi2) => ->. rewrite ssrnat.ltnS. apply Nat.lt_le_incl in Hi2. by move /ssrnat.leP :Hi2 => ->. intro Hi2 ; rewrite Hi2. unfold ith_step. rewrite SF_lx_rcons. rewrite SF_ly_rcons. replace (nth 0 (rcons (SF_lx s') (fst (b' + e, b'))) (S (SF_size s'))) with (b' + e). replace (nth 0 (rcons (SF_lx s') (fst (b' + e, b'))) (SF_size s')) with b'. replace (nth 0 (rcons (SF_ly s') (snd (b' + e, b'))) (SF_size s')) with b'. rewrite Rplus_comm. unfold Rminus. rewrite Rplus_assoc ; rewrite Rplus_opp_r ; rewrite Rplus_0_r. apply Rle_lt_trans with (delta b' / 2). assumption. apply Rminus_lt_0 ; field_simplify ; rewrite ?Rdiv_1. by apply is_pos_div_2. replace (SF_size s') with (Peano.pred (size (rcons (SF_ly s') (snd (b' + e, b'))))). rewrite nth_last. rewrite last_rcons. easy. rewrite size_rcons ; rewrite SF_size_ly ; simpl ; easy. rewrite nth_rcons. rewrite SF_size_lx. rewrite ssrnat.leqnn. replace (SF_size s') with (Peano.pred (size (SF_lx s'))). rewrite nth_last. destruct HH as (HH, HH') ; rewrite <- HH'. case Hcase2 : (SF_lx s'). assert (size (SF_lx s') = S (SF_size s')) as Hss. apply SF_size_lx. rewrite Hcase2 in Hss. apply O_S in Hss ; destruct Hss. rewrite last_cons ; rewrite last_cons ; easy. rewrite SF_size_lx ; simpl ; easy. replace (S (SF_size s')) with (Peano.pred (size (rcons (SF_lx s') (fst (b' + e, b'))))). rewrite nth_last ; rewrite last_rcons ; easy. rewrite size_rcons ; rewrite SF_size_lx ; simpl ; easy. rewrite SF_lx_rcons ; rewrite last_rcons. split. unfold SF_rcons ; simpl. apply H5. easy. apply H in H42. assert (b' < b' + e) as H43. rewrite <- (Rplus_0_r b') at 1. now apply Rplus_lt_compat_l. apply Rle_not_lt in H42. contradiction. apply Hb'3. assert (b' <= Rmax a b) as Hb'3. apply H. intros x Hx. apply Hx. apply Rle_not_gt in Hb'3. contradiction. Qed.
imports: Coq(Reals ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy SF_seq RInt