proposition: Lemma modsym_mod_compat : forall x m, (modsym x m) mod m = x mod m.
proof: Proof. intros x m; unfold modsym. rewrite Zminus_mod_idemp_l. f_equal; ring. Qed.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm Znumfacts