proposition: Lemma eqmod_add_idemp_r n i j k : (i + k) mod n = (j + k) mod n <-> i mod n = j mod n.
proof: Proof. by rewrite <- !(Nat.add_comm k); apply eqmod_add_idemp_l. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnRewrite