proposition: Lemma Zgcd_gcd_rl : forall a b : Z, Zgcd a (Zgcd a b) = Zgcd a b.
proof: Proof. intros a b. case (Zdec a). intro H0; rewrite H0; repeat rewrite Zgcd_zero_lft; auto with zarith. intro H0. replace (Zgcd a b) with (Z.abs (Zgcd a b)). rewrite Zgcd_abs. replace (Z.abs (Z.abs (Zgcd a b))) with (Zgcd a b). apply Zgcd_divisor. auto with zarith. apply Zdivides_abs_elim_rht. apply Zgcd_is_divisor_lft. generalize (Zgcd_nonneg a b); rewrite Zabs_idemp; auto with zarith. generalize (Zgcd_nonneg a b); auto with zarith. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)