proposition: Lemma modsym_mod_diff : forall x m, 0 < m -> { k | modsym x m = x mod m + m * k }.
proof: Proof. intros x m. exists ((modsym x m - x mod m) / m). rewrite Z_mult_div_mod; [ | auto with * ]. rewrite Zminus_mod, modsym_mod_compat. rewrite Zminus_mod_idemp_l. do 2 rewrite Zminus_mod_idemp_r. rewrite Z.sub_diag, Zmod_0_l. ring. Qed.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm Znumfacts