proposition: Lemma min_cycle1 X (r r' : relation X) (d : X -> Prop) nd (ND: nd = fun x => ~ d x) (TOT: is_total d r') (T : transitive r') (INCL: r' ⊆ r⁺) (INV: irreflexive (r ⨾ r')) : acyclic r <-> acyclic (⦗nd⦘ ⨾ r ⨾ ⦗nd⦘) /\ irreflexive (⦗d⦘ ⨾ r ⨾ ⦗d⦘) /\ irreflexive (⦗nd⦘ ⨾ r ⨾ ⦗d⦘ ⨾ r'^? ⨾ ⦗d⦘ ⨾ r ⨾ ⦗nd⦘ ⨾ (⦗nd⦘ ⨾ r ⨾ ⦗nd⦘)＊).
proof: Proof. assert (AA: restr_rel nd r ≡ ⦗nd⦘⨾ r⨾ ⦗nd⦘). by red; unfold seq, eqv_rel, restr_rel, inclusion in *; split; ins; desf; eauto 10. forward (eapply min_cycle; eauto) as N; subst; rewrite N, <- !AA; clear. unfold irreflexive, seq, eqv_rel; split; ins; desf; splits; ins; desf; eauto. by eapply H0; eauto 10. by apply (H1 c1); repeat eexists; eauto. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnRewrite