proposition: Lemma ISMod_union : exists f', exists g', ISMod E R f' g' /\ forall i, (exists k, g' i = g k) /\ (exists k, f' i = f k).
proof: Proof. pose (reid := rec_ch_min _ hyp2). pose (g0 := fun i => (g (reid i))). pose (f0 := fun i => match i with 0 => f 0 | S j => (f (S (reid j))) end). pose (P := fun i j => i <= j /\ (R (g j) (f (S j)))). assert (E_gfi : forall i j, S (reid i) <= j -> j < (reid (S i)) -> E (g j) (f (S j))). intros i j le_Sij lt_jx. gen (is_min_ch (P (S (reid i))) (hyp2 (S (reid i)))). unfold P. intros Hproj. gen (Hproj j). intros HT. destruct (hyp1 j) as [_ ERj]. destruct ERj; auto. destruct (NatCompat.lt_not_le lt_jx). apply HT. auto. assert (E_gf0 : forall j, j < (reid 0) -> E (g j) (f (S j))). intros j lt_jx. gen (is_min_ch (P 0) (hyp2 0)). unfold P. intro HP. gen (HP j). intro HPj. destruct (hyp1 j) as [_ ERj]. destruct ERj; auto. destruct (NatCompat.lt_not_le lt_jx). apply HPj. split; auto. lia. assert (HEfgi : forall i j k, S (reid i) <= j -> j <= k -> k <= reid (S i) -> E (f j) (g k)). intros i j k le_ij le_jk le_ki. induction k. rewrite (proj1 (Nat.le_0_r _) le_jk) in le_ij. destruct (Nat.nle_succ_0 _ le_ij). destruct (NatCompat.le_lt_or_eq le_jk) as [HT | HT]. 2: { rewrite HT. apply (proj1 (hyp1 (S k))). } apply TE with (g k). exact (IHk (NatCompat.lt_n_Sm_le HT) (Nat.le_trans (Nat.le_succ_diag_r k) le_ki)). apply TE with (f (S k)). apply (E_gfi i k); try lia. apply (proj1 (hyp1 (S k))). assert (HEfg0 : forall j k, j <= k -> k <= reid 0 -> E (f j) (g k)). intros j k le_jk le_k0. induction k. rewrite (proj1 (Nat.le_0_r _) le_jk). apply (proj1 (hyp1 0)). destruct (NatCompat.le_lt_or_eq le_jk) as [HT | HT]. 2: { rewrite HT. apply (proj1 (hyp1 (S k))). } apply TE with (g k). apply IHk; lia. apply TE with (f (S k)). apply (E_gf0 k); try lia. apply (proj1 (hyp1 (S k))). assert (Rgf : forall i, R (g (reid i)) (f (S (reid i)))). intro i. induction i. 2: { destruct (rec_ch_minP P hyp2 i). hyp. } simpl. destruct (ch_minP (P 0) (hyp2 0)). hyp. exists f0; exists g0. split. 2: { intro. split. exists (reid i). auto. destruct i. exists 0; auto. exists (S (reid i)). auto. } intro. split. 2: { apply Rgf. } destruct i. 2: { unfold f0, g0. apply (HEfgi i); auto. destruct (ch_minP (P (S (reid i))) (hyp2 (S (reid i)))) as [? _]. hyp. } unfold f0, g0. apply HEfg0; lia. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)