proposition: Lemma mod_eq_plus_invert : forall x : Z, sig (fun y => (x + y) %= 0).
proof: Proof. intros; exists (-x); ring_simplify; apply mod_eq_refl. Qed.
imports: Arith ZArith RelationClasses Type_class_definition Lia ZArith Znumtheory