proposition: Lemma deprecated_Zis_gcd_for_euclid : forall a b d q:Z, Zis_gcd b (a - q * b) d -> Zis_gcd a b d.
proof: Proof. intros a b d q; simple induction 1; constructor; intuition. replace a with (a - q * b + q * b). - auto with zarith. - ring. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat