proposition: Lemma Zgcdn_ok_before_fibonacci : forall n a b, 0 < a < b -> a < fibonacci (S n) -> Zis_gcd a b (Zgcdn n a b).
proof: Proof. intros n a; destruct a as [|p|p]. 1,3 : intros; lia. cut (forall k n b, k = (S (Pos.to_nat p) - n)%nat -> 0 < Zpos p < b -> Zpos p < fibonacci (S n) -> Zis_gcd (Zpos p) b (Zgcdn n (Zpos p) b)). - destruct 2; eauto. - clear n; intros k; induction k as [|k IHk]. + intros. apply Zgcdn_linear_bound. lia. + intros n b H H0 H1. generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros H2. assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)) as H3. * apply IHk; auto. -- lia. -- replace (fibonacci (S (S n))) with (fibonacci (S n)+fibonacci n) by auto. generalize (fibonacci_pos n); lia. * replace (Zgcdn n (Zpos p) b) with (Zgcdn (S n) (Zpos p) b); auto. generalize (H2 H3); clear H2 H3; lia. Qed.
imports: ZArith_base ZArithRing Zdiv Znumtheory Lia