proposition: Lemma Zgcd_idemp : forall a : Z, (a > 0)%Z -> Zgcd a a = a.
proof: Proof. intros a Ha. rewrite Zgcd_rec. rewrite Z_mod_same. rewrite Zgcd_zero_rht. auto with zarith. replace (Z.abs a) with a. assumption. symmetry in |- *; auto with zarith. auto with zarith. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)