proposition: Lemma acyclic_union_singl_max A (r : relation A) a b (MAX: max_elt r b) : acyclic (r ∪ singl_rel a b) <-> acyclic r /\ a <> b.
proof: Proof. rewrite acyclic_union_singl; intuition; desf; eauto using rt_refl. apply rt_begin in H; unfolder in H; desf; eauto. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath