proposition: Lemma functional_path_transp A (s: relation A) (FUN: functional s⁻¹): s＊⨾ s⁻¹＊ ⊆ s＊ ∪ (s⁻¹)＊.
proof: Proof. rewrite functional_path with (s:=s⁻¹); [rels|done]. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn