proposition: Lemma modsym_bounds : forall x m, 0 < m -> - m <= 2 * modsym x m < m.
proof: Proof. intros x m Pm; unfold modsym. pose proof Z_mod_lt (x + m / 2) m. pose proof Z_mod_lt m 2. split; ring_simplify; rewrite Z_mult_div_mod; lia. Qed.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm Znumfacts