proposition: Lemma Zdivides_dec : forall a b : Z, {Zdivides a b} + {~ Zdivides a b}.
proof: Proof. intros a b. case (Zdec b). intro Hb. rewrite Hb. left. apply Zdivides_zero_rht. intro Hb. case (Zdec a). intro Ha. rewrite Ha. right. intro H0. rewrite (Zdivides_zero_lft b H0) in Hb. elim Hb. auto. intro Ha. generalize (Zdivides_Zmod0 b a Ha). generalize (Zmod0_Zdivides b a Ha). case (Zdec (b mod a)); auto. Qed.
imports: CoRN.model.Zmod.ZBasics