proposition: Lemma acyclic_minimize X (r : relation X) : acyclic r <-> ~ exists f n, << ENDS: f 0 = f (S n) >> /\ << STEP: forall i (LT: i <= n), r (f i) (f (S i)) >> /\ << MIN: forall i (LTi: i <= n) j (LTj: j <= S n), r (f i) (f j) -> j = S i \/ i = n /\ j = 0 >> /\ << NODUP: forall i (LTi: i <= S n) j (LTj: j <= S n), f i = f j -> i = j \/ i = 0 /\ j = S n \/ i = S n /\ j = 0 >>.
proof: Proof. rewrite acyclic_minimize1. split; intros A B; destruct A; desc; unnw; eauto. exists f, n; repeat split; ins; eauto. destruct (lt_dec i j). destruct j; [exfalso; lia|]; ins; auto. specialize (STEP j); specialize_full STEP; try lia. rewrite <- H in STEP; eapply MIN in STEP; try lia. destruct (lt_dec j i); try lia. destruct i; [exfalso; lia|]; ins; auto. specialize (STEP i); specialize_full STEP; try lia. rewrite H in STEP; eapply MIN in STEP; try lia. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnRewrite