proposition: Lemma moddec : forall (a b : Z) (n : nat), Mod a b n \/ ~ Mod a b n.
proof: Proof. intros. elim (moddivmin a b n). intros. elim (divdec (Z.abs_nat (a - b)) n). left. apply H0. assumption. right. intro. elim H1. apply H. assumption. Qed.
imports: ZArith lemmas natZ exp divides