proposition: Lemma euclid_gcd1 : forall (d : nat) (x y q r : Z), Zis_gcd x y (Z.of_nat d) -> x = (q * y + r)%Z -> Zis_gcd r y (Z.of_nat d).
proof: Proof. intros. rewrite H0 in H. clear H0 x. replace r with (y * - q + (q * y + r))%Z by lia. apply Zis_gcd_sym. apply Zis_gcd_for_euclid2; auto with zarith. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow