proposition: Lemma cycle_decomp_u1 A (r : relation A) a b c : (r ∪ singl_rel a b)⁺ c c -> r⁺ c c \/ r＊ b a.
proof: Proof. ins; apply ct_union_singl in H; unfolder in H. desf; eauto using clos_refl_trans. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath