proposition: Lemma Zgcdn_linear_bound : forall n a b, Z.abs a < Z.of_nat n -> Zis_gcd a b (Zgcdn n a b).
proof: Proof. intros n; induction n as [|n IHn]. - intros; lia. - intros a; destruct a as [|p|p]; intros b H; simpl; [ generalize (Zis_gcd_0_abs b); intuition | | ]; unfold Z.modulo; generalize (Z_div_mod b (Zpos p) (eq_refl Gt)); destruct (Z.div_eucl b (Zpos p)) as (q,r); intros (H0,H1); rewrite Nat2Z.inj_succ in H; simpl Z.abs in H; (assert (H2: Z.abs r < Z.of_nat n) by lia); assert (IH:=IHn r (Zpos p) H2); clear IHn; simpl in IH |- *; rewrite H0. + apply Zis_gcd_for_euclid2; auto. + apply Zis_gcd_minus; apply Zis_gcd_sym. apply Zis_gcd_for_euclid2; auto. Qed.
imports: ZArith_base ZArithRing Zdiv Znumtheory Lia