proposition: Lemma wf_union_absorb : WF R -> WF S -> R @ S << R -> WF (R U S).
proof: Proof. intros R_wf S_wf RS x. apply notNT_SN. intros [f [f1 f2]]. assert (a1 : forall i, exists j, i < j /\ R (f j) (f (1+j))). apply NNPP. rewrite not_forall_eq. intros [i0 hi0]. rewrite not_exists_eq in hi0. assert (hi0' : forall i, i0 < i -> S (f i) (f (1+i))). intros i ii0. gen (hi0 i). rewrite not_and_eq. fo. absurd (NT S (f (i0+1))). apply SN_notNT. fo. exists (fun i => f (i+(i0+1))). split. refl. intro i. apply hi0'. lia. assert (a2 : forall i, exists j, i < j /\ R (f j) (f (1+j)) /\ forall k, i < k < j -> S (f k) (f (1+k))). intro i. gen (ch_min (a1 i)); intros [j [[[j1 j2] j3] j4]]. ex j. split. hyp. split. hyp. intros k ikj. destruct (f2 k). 2: hyp. assert (j <= k). apply j3. fo. lia. destruct (a2 0) as [i0 [i0h [i0r i0s]]]. destruct (dep_choice i0 a2) as [b [b1 b2]]. assert (a3 : NT (R @ S#) (f i0)). ex (fun i => f (b i)). split. rewrite b2. refl. intro i. ex (f (1 + b i)). split. destruct i. rewrite b2. hyp. gen (b1 i). fo. apply rtc_intro_seq. gen (b1 i). lia. intros k hk. gen (b1 i). intros [c1 [c2 c3]]. apply c3. lia. revert a3. apply SN_notNT. apply (SN_incl R). apply absorbs_right_rtc. hyp. fo. Qed.
imports: Coq(Lia Wellfounded.Union) CoLoR(SN RelUtil LogicUtil AccUtil NotSN_IS ClassicUtil LeastNat DepChoice)