proposition: Lemma acyclic_seq_from_union A (r1 r2: relation A): acyclic (r1 ∪ r2) -> acyclic (r1⨾ r2).
proof: Proof. ins. arewrite (r1 ⊆ r1 ∪ r2). arewrite (r2 ⊆ r1 ∪ r2) at 2. rewrite (ct_step (r1 ∪ r2)). rewrite inclusion_t_rt at 1. relsf. red; rels. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath