proposition: Lemma Zis_gcd_unique : forall a b d e : Z, Zis_gcd a b d -> Zis_gcd a b e -> d = e.
proof: Proof. intros a b d e. unfold Zis_gcd in |- *. intros Hd He. elim Hd; intros Hdl Hdr. elim He; intros Hel Her. induction a as [| p| p]. induction b as [| p| p]. transitivity 0%Z. apply Hdl; reflexivity; reflexivity. symmetry in |- *. apply Hel; reflexivity; reflexivity. elim Hdr. intros Hd0 Hddiv. elim Her. intros He0 Hediv. elim Hddiv; intros _ Hddiv2. elim Hddiv2; intros _ Hdgcd. elim Hediv; intros _ Hediv2. elim Hediv2; intros _ Hegcd. apply (Zdivides_antisymm _ _ Hd0 He0). apply Hegcd; tauto. apply Hdgcd; tauto. right; discriminate. right; discriminate. elim Hdr. intros Hd0 Hddiv. elim Her. intros He0 Hediv. elim Hddiv; intros _ Hddiv2. elim Hddiv2; intros _ Hdgcd. elim Hediv; intros _ Hediv2. elim Hediv2; intros _ Hegcd. apply (Zdivides_antisymm _ _ Hd0 He0). apply Hegcd; tauto. apply Hdgcd; tauto. right. discriminate. right. discriminate. elim Hdr. intros Hd0 Hddiv. elim Her. intros He0 Hediv. elim Hddiv; intros _ Hddiv2. elim Hddiv2; intros _ Hdgcd. elim Hediv; intros _ Hediv2. elim Hediv2; intros _ Hegcd. apply (Zdivides_antisymm _ _ Hd0 He0). apply Hegcd; tauto. apply Hdgcd; tauto. left. discriminate. left. discriminate. elim Hdr. intros Hd0 Hddiv. elim Her. intros He0 Hediv. elim Hddiv; intros _ Hddiv2. elim Hddiv2; intros _ Hdgcd. elim Hediv; intros _ Hediv2. elim Hediv2; intros _ Hegcd. apply (Zdivides_antisymm _ _ Hd0 He0). apply Hegcd; tauto. apply Hdgcd; tauto. left. discriminate. left. discriminate. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)