proposition: Lemma Zmodap_tight_apart: (tight_apart ZModeq ZModap).
proof: Proof. red. intros x y. split. elim (Zmodeq_dec m x y). intros H Hnn. exact H. intros Hn Hnn. elim Hnn. intro H. elim Hn. exact H. intro H. intro Hnn. elim Hnn. exact H. Qed.
imports: CoRN.model.Zmod.ZMod CoRN.algebra.CFields