proposition: Lemma sn_comm_sntr : forall x, SN R x -> (forall y, R#1 x y -> SN S y) -> S@R << R!1@S#1 -> SN (R!1 U S!1) x.
proof: Proof. intros x snr sns comm. assert (snrt := SN_tc1 snr); clear snr. induction snrt as [x _ IHr]. apply SN_intro. intros y xRSy. destruct xRSy as [xRy | xSy]. apply IHr. hyp. assert (SN (S!1) y) as sny. apply SN_tc1. apply sns. apply tc1_incl_rtc1; hyp. intros y0 yRy0. apply sns. apply trans_comp_incl. class. exists y; split; trivial. apply tc1_incl_rtc1. hyp. assert (SN (S!1) y) as sny. apply SN_tc1. apply SN_inv_rtc1 with x. apply tc1_incl_rtc1. hyp. apply sns. refl. induction sny as [y _ IHs]. apply SN_intro. intros z yRSz. destruct yRSz as [yRz | ySz]. assert ((R!1 @ (R U S)#1) x z) as xRz. apply comm_s_r; trivial. destruct yRz as [y z yRz | y m z yRm mRz]. exists z. split. exists y. split; trivial. apply union_rel_rt1_right. apply tc1_incl_rtc1. hyp. refl. exists m. split. exists y. split; trivial. apply union_rel_rt1_right. apply tc1_incl_rtc1. hyp. apply union_rel_rt1_left. apply tc1_incl_rtc1. hyp. destruct xRz as [m [xRm mz]]. assert (SN (R!1 U S!1) m) as SNm. apply IHr. hyp. intros y0 mRy0. apply sns. apply trans_comp_incl. class. exists m. split; trivial. apply tc1_incl_rtc1. hyp. apply SN_inv_rtc1 with m. apply incl_union_rt1_union. hyp. hyp. apply IHs; trivial. trans y; trivial. Qed.
imports: Coq(Lia Wellfounded.Union) CoLoR(SN RelUtil LogicUtil AccUtil NotSN_IS ClassicUtil LeastNat DepChoice)