proposition: Lemma p_gcd_is_divisor : forall a b : positive, Zdivides (Zpos (p_gcd a b)) (Zpos a) /\ Zdivides (Zpos (p_gcd a b)) (Zpos b).
proof: Proof. intros a b. apply (pp_gcd_is_divisor (a, b)). Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)