proposition: Lemma Zgcd_symm : forall a b : Z, Zgcd a b = Zgcd b a.
proof: Proof. intros a b. case a; case b; simpl in |- *; intros; unfold Zgcd, Zgcd_duv in |- *; try rewrite p_gcd_symm; auto. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)