proposition: Lemma last_exists_rewrite A dom (s: relation A) (ACYC: acyclic s) (IN: s ⊆ ⦗fun x : A => In x dom⦘ ⨾ s ⨾ ⦗fun x : A => In x dom⦘): ⦗fun _ => True⦘ ⊆ s＊ ⨾ ⦗max_elt s⦘ ⨾ s⁻¹＊.
proof: Proof. unfold inclusion, eqv_rel, seq; ins; desf. destruct (classic (In y dom)) as [INy|NINy]; cycle 1. - exists y; splits; vauto. exists y; splits; vauto. red; ins; apply IN in REL; revert REL; basic_solver. - generalize (last_exists dom ACYC (dom_helper dom IN INy)); ins; desc. exists b; splits; eauto. exists b; splits; eauto. apply transp_rt with (r:=s); vauto. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn