proposition: Lemma p_gcd_symm : forall a b : positive, p_gcd a b = p_gcd b a.
proof: Proof. intros a b. case (Zdec (Zpos a - Zpos b)). intro H0. cut (Zpos a = Zpos b). intro Heq. inversion Heq. reflexivity. auto with zarith. intro Hdiff. cut (a <> b). intro Hneq. unfold p_gcd in |- *. rewrite (p_gcd_duv_symm a b Hneq). auto. intro Hfalse. apply Hdiff. rewrite Hfalse. auto with zarith. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)