proposition: Lemma Zgcd_zero : forall a b : Z, Zgcd a b = 0%Z -> a = 0%Z /\ b = 0%Z.
proof: Proof. intros a b. case a; case b; unfold Zgcd in |- *; simpl in |- *; intros; try discriminate; try tauto. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)