proposition: Lemma zmoddec : forall a b n : Z, ZMod a b n \/ ~ ZMod a b n.
proof: Proof. intros. elim (zmoddivmin a b n). intros. elim (zdivdec (a - b) n). left. apply H0. assumption. right. intro. elim H1. apply H. assumption. Qed.
imports: ZArith lemmas natZ exp divides