proposition: Lemma min_cycle_step X (r : relation X) f n (MC : min_cycle_mod r f n) i j : r (f i) (f j) <-> j mod n = S i mod n.
proof: Proof. destruct MC as [NZ MOD STEP MIN]; split; ins; eauto. by rewrite (MOD i), (MOD j), H, <- !MOD; auto. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnRewrite