proposition: Lemma acyclic_utd : forall r (ACYC: acyclic r) r' (T: transitive r') (IRR: irreflexive r') dom (F: is_total dom r') (DB: domb r' dom) (I': irreflexive (r' ⨾ r⁺)), acyclic (r ∪ r').
proof: Proof. ins; eapply acyclic_union_total_r; splits; eauto using trans_irr_acyclic. rewrite irreflexive_seqC; relsf. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath