proposition: Lemma IS_tc : exists h', IS E h' /\ h' 0 = h 0.
proof: Proof. assert (exPath : forall i, exists l, path E (h i) (h (S i)) l). intros i. apply clos_trans_path; auto. pose (li := fun i => proj1_sig (constructive_indefinite_description _ (exPath i))). pose (F := fun i => length (cons (h i) (li i))). assert (HFi : forall i, exists y, F i = S y). intro i. exists (length (li i)). auto. pose (F0 := fun i => Interval_list F i). pose (P := fun i j => fst (F0 j) <= i /\ i < snd (F0 j)). assert (HinT : forall k, fst (F0 k) < snd (F0 k)). induction k. simpl. destruct (HFi 0) as [y Hy]; rewrite Hy; lia. simpl. destruct (HFi (S k)) as [y Hy]; rewrite Hy; lia. assert (HPeq : forall i j k, P k i /\ P k j -> i = j). intros i j k H; unfold P in H. destruct H as [H H0]. destruct H0 as [H1 H2]. destruct H as [H H0]. gen (Nat.le_lt_trans H H2). intros H3. gen (Nat.le_lt_trans H1 H0). intros H4. destruct (Nat.le_gt_cases i j) as [H5 | H5]. case (NatCompat.le_lt_or_eq H5); try auto. clear H5 H1 H2 H3; intros H5. induction j. lia. simpl in H4. case (NatCompat.le_lt_or_eq (NatCompat.lt_n_Sm_le H5)); intros H1. rewrite (IHj (Nat.lt_trans (HinT j) H4) H1) in H1. lia. rewrite H1 in H4. lia. clear H1 H2 H4 H H0. induction i. lia. simpl in H3. case (NatCompat.le_lt_or_eq (NatCompat.lt_n_Sm_le H5)); intros H1. rewrite (IHi (Nat.lt_trans (HinT i) H3) H1) in H1. lia. rewrite H1 in H3; lia. assert (exP_F0 : forall i, exists j, P i j). intros i. apply int_exPi. auto. pose (F1 := fun i => proj1_sig (ch_min (exP_F0 i))). assert (HF0 : forall i, (snd (F0 i) - fst (F0 i) = F i)). induction i; auto. simpl. lia. pose (h' := fun i => let j := (F1 i) in let i' := i - (fst (F0 j)) in nth i' (h j :: li j) (h (S j))). assert (HT : forall i, F1 i <= F1 (S i) <= S (F1 i)). intros. assert (HSi : S i <= snd (F0 (F1 i))). gen (ch_minP _ (exP_F0 i)). unfold P. intuition. destruct (NatCompat.le_lt_or_eq HSi) as [H0 | H0]. 2: { assert (PSi : P (S i) (S (F1 i))). unfold P. simpl. rewrite H0. split; try lia. destruct (HFi (S (F1 i))) as [y Hy]. rewrite Hy; lia. cut (F1 (S i) = S (F1 i)). intros HT; rewrite HT. split; lia. destruct (proj2_sig (ch_min (exP_F0 (S i)))) as [_ H1]. apply H1. split; auto. intros k. unfold P. intros H2. rewrite (HPeq _ _ _ (conj PSi H2)). lia. } cut (F1 (S i) = F1 i). intros HT; rewrite HT. split; lia. assert (PSi : P (S i) (F1 i)). split; try lia. apply (@Nat.le_trans _ i); try lia. destruct (ch_minP _ (exP_F0 i)); hyp. destruct (proj2_sig (ch_min (exP_F0 (S i)))) as [_ H]. apply H; split; try hyp. intros k Hk. rewrite (HPeq _ _ _ (conj PSi Hk)). lia. assert (DecFSi : forall i, F1 (S i) = F1 i \/ F1 (S i) = S (F1 i)). intros. destruct (HT i) as [Hi1 Hi2]. lia. assert (forall i, i - fst (F0 (F1 i)) < length (h (F1 i) :: li (F1 i))). intros i. destruct (ch_minP _ (exP_F0 i)) as [H1 H2]. assert (H0 : i - fst (F0 (F1 i)) < snd (F0 (F1 i)) - fst (F0 (F1 i))). apply Nat.add_lt_mono_l with (p := fst (F0 (F1 i))). rewrite Nat.add_comm, Nat.sub_add; auto. rewrite Nat.add_comm, Nat.sub_add; auto. apply (Nat.le_trans H1 (@Nat.lt_le_incl _ _ H2)). apply (Nat.lt_le_trans H0). rewrite (HF0 (F1 i)). auto. exists h'; split; unfold h'. intro i; destruct (DecFSi i) as [Hi | Hi]; rewrite Hi. assert (S (i - fst (F0 (F1 i))) < length (h (F1 i) :: li (F1 i))). gen (H (S i)). rewrite Hi, Nat.sub_succ_l. auto. destruct (ch_minP _ (exP_F0 i)). auto. rewrite Nat.sub_succ_l. 2: { apply (proj1 (ch_minP _ (exP_F0 i))). } gen H0. set (k := i - fst (F0 (F1 i))). destruct k. simpl. intros. apply path_headP. apply (proj2_sig (constructive_indefinite_description _ (exPath (F1 i)))). simpl. intros. apply path_nth_inP with (x := (h (F1 i))); try lia. apply (proj2_sig (constructive_indefinite_description _ (exPath (F1 i)))). rewrite <- Hi. assert (S i = snd (F0 (F1 i))). destruct (ch_minP _ (exP_F0 i)) as [_ HT0]. destruct (NatCompat.le_lt_or_eq (NatCompat.lt_le_S HT0)); try auto. cut (F1 (S i) = F1 i). rewrite Hi. intros. symmetry in H1. lia. assert (PSi : P (S i) (F1 i)). split; try lia; auto. apply (@Nat.le_trans _ i); try lia. destruct (ch_minP _ (exP_F0 i)); hyp. destruct (proj2_sig (ch_min (exP_F0 (S i)))) as [_ H1]. apply H1; split; try hyp. intros k Hk. rewrite (HPeq _ _ _ (conj PSi Hk)). lia. assert (nth (S i - fst (F0 (F1 (S i)))) (h (F1 (S i)) :: li (F1 (S i))) (h (S (F1 (S i)))) = h (F1 (S i))). cut (S i - fst (F0 (F1 (S i))) = 0). intros. rewrite H1. simpl; auto. rewrite Hi, H0. simpl. lia. rewrite H1. clear H1. gen (HF0 (F1 i)). unfold F. intros. cut (i - fst (F0 (F1 i)) = length (li (F1 i))). 2: { rewrite <- H0, Nat.sub_succ_l in H1. simpl in H1. lia. apply (proj1 (ch_minP _ (exP_F0 i))). } set (k := i - fst (F0 (F1 i))). assert (path E (h (F1 i)) (h (S (F1 i))) (li (F1 i))). apply (proj2_sig (constructive_indefinite_description _ (exPath (F1 i)))). destruct k. intros. symmetry in H3. destruct (li (F1 i)). simpl. simpl in H3. rewrite Hi. auto. simpl in H3. lia. simpl. intros. apply path_lastP with (x := (h (F1 i))); auto. rewrite Hi. hyp. cut ((F1 0) = 0). intro H0; rewrite H0; refl. assert (P00 : P 0 0). unfold P. simpl. split; try lia. destruct (HFi 0) as [k Hk]. rewrite Hk; lia. apply Nat.le_0_r. apply (is_min_ch (P 0) (exP_F0 0) 0 P00). Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)