proposition: Lemma Zmodap_cotransitive: (cotransitive ZModap).
proof: Proof. red. intros x y H. intros z. elim (Zmodeq_dec m x z). elim (Zmodeq_dec m y z). intros Hyz Hxz. elim H. apply (Zmodeq_trans _ _ _ _ Hxz (Zmodeq_symm _ _ _ Hyz)). intros _ Hxz. right. intro Hzy. apply H. apply (Zmodeq_trans _ _ _ _ Hxz Hzy). intro H_xz. left. intro Hxz. elim H_xz. exact Hxz. Qed.
imports: CoRN.model.Zmod.ZMod CoRN.algebra.CFields