proposition: Lemma mod_SS_expand i n : (S i mod S n) = if eq_op n 0 then 0 else if eq_op (i mod (S n)) n then 0 else S (i mod (S n)).
proof: Proof. by rewrite mod_S_expand; desf. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnRewrite