proposition: Lemma acyclic_no_min_cycle X (r : relation X) : acyclic r <-> ~ exists f n, min_cycle_mod r f n.
proof: Proof. rewrite acyclic_minimize1; split; intros A B; destruct A; desc. { destruct B as [NZ MOD STEP MIN]; destruct n; try done. exists f, n; unnw; repeat split; intros; try done; eauto. by rewrite (MOD (S n)), Nat.mod_same. apply MIN in H. destruct (eqP i n), (eqP j (S n)); subst; auto; rewrite ?Nat.mod_same, ?Nat.mod_small in H; lia. } exists (fun x => f (x mod (S n))), (S n); split; intros; try done. - by rewrite Nat.mod_mod. - assert (UB := Nat.mod_upper_bound i (S n)). forward apply (STEP (i mod S n)); try lia. rewrite mod_SS_expand; desf; desf. by rewrite !Nat.mod_1_r, ENDS. by rewrite Heq0, ENDS. - assert (UBi := Nat.mod_upper_bound i (S n)). assert (UBj := Nat.mod_upper_bound j (S n)). apply MIN in H; try lia. rewrite mod_SS_expand; desf; desf; lia. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnRewrite