proposition: Lemma in_pref_union : forall X (r r' : relation X) (dom : X -> Prop) (IRR: irreflexive r) (T: transitive r) (TOT: is_total dom r) (DL: forall x y (R: r' x y), dom x /\ ~ dom y) x y (R: clos_trans (pref_union r r') x y) (D: dom y), r x y.
proof: Proof. unfold pref_union; ins; apply clos_trans_t1n in R; induction R; desf; eauto. by eapply DL in H; desf. apply clos_t1n_trans in R. assert (K:=DL _ _ H); desc. destruct (classic (x = z)) as [|N]; [|apply TOT in N]; desf; ins. by exfalso; eauto. exfalso; eapply acyclic_pref_union with (r:=r), t_trans, t_trans; vauto. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath