proposition: Lemma min_cycle_wlog X (r : relation X) f n (MC : min_cycle_mod r f n) i (P : X -> Prop) (PROP: P (f i)) : exists f, << MC : min_cycle_mod r f n >> /\ << PROP : P (f 0) >>.
proof: Proof. exists (fun x => f (x + i)); unnw; repeat split; ins; try apply MC. by rewrite !(mp_modulo MC (_ + i)), Nat.add_mod_idemp_l; try apply MC. eby rewrite (min_cycle_step MC) in *; eapply eqmod_add_idemp_r. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnRewrite