proposition: Lemma last_exists A dom (s: relation A) (ACYC: acyclic s) a (DOM: forall c, s＊ a c -> In c dom): exists b, s＊ a b /\ max_elt s b.
proof: Proof. revert a DOM. induction dom using (well_founded_ind (well_founded_ltof _ (@length _))). ins; destruct (classic (exists a1, s a a1)); cycle 1. by exists a; eexists; splits; [vauto| red; eauto]. assert (INa: In a dom). by apply DOM; vauto. desc; apply in_split in INa; desf. assert(exists b, s ＊ a1 b /\ max_elt s b). { eapply (H (l1 ++ l2)). * unfold ltof; rewrite !app_length; simpl; lia. * ins. assert(INc: In c (l1 ++ a :: l2)). by eapply DOM; eapply rt_trans; vauto. rewrite in_app_iff in *; simpls; desf; eauto. exfalso; eapply ACYC; eapply t_step_rt; eauto. } unfold seq in *; desc; exists b; splits; try done. apply rt_begin; right; eexists; eauto. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn