proposition: Lemma Zis_gcd_for_euclid2 : forall b d q r:Z, Zis_gcd r b d -> Zis_gcd b (b * q + r) d.
proof: Proof. intros b d q r; destruct 1 as [? ? H]; constructor; intuition. apply H; auto. replace r with (b * q + r - b * q). - auto with zarith. - ring. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat