proposition: Lemma Zgcd_nonzero : forall a b : Z, 0%Z <> Zgcd a b -> a <> 0%Z \/ b <> 0%Z.
proof: Proof. intros a b. case a. case b. rewrite Zgcd_zero_rht; simpl in |- *; tauto. intros; right; intro; discriminate. intros; right; intro; discriminate. intros; left; intro; discriminate. intros; left; intro; discriminate. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)