proposition: Lemma Zgcd_gcd_lr : forall a b : Z, Zgcd (Zgcd a b) b = Zgcd a b.
proof: Proof. intros a b; rewrite (Zgcd_symm a b); rewrite (Zgcd_symm (Zgcd b a) b); apply Zgcd_gcd_rl. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)