proposition: Lemma min_cycle_nodup X (r : relation X) f n (MC : min_cycle_mod r f n) i j (EQ: f i = f j) : i mod n = j mod n.
proof: Proof. apply eqmod_S. by erewrite <- (mp_min MC); [|rewrite EQ; apply (mp_step MC)]. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnRewrite