proposition: Lemma Zgcd_one_lft : forall a : Z, Zgcd 1 a = 1%Z.
proof: Proof. intro a. generalize (Zgcd_is_divisor_lft 1 a). cut (0 < Zgcd 1 a)%Z. auto with zarith. apply Zgcd_pos. left; intro; discriminate. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)