proposition: Lemma last_functional A (s: relation A) (FUN: functional s): functional (s＊ ⨾ ⦗max_elt s⦘).
proof: Proof. apply functional_alt. rewrite transp_seq; relsf. rewrite !seqA, transp_rt. sin_rewrite functional_path; [relsf | done]. seq_rewrite seq_eqv_max_rt; rels. seq_rewrite transp_seq_eqv_max_rt; rels. basic_solver. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn