proposition: Lemma Zgcdn_worst_is_fibonacci : forall n a b, 0 < a < b -> Zis_gcd a b (Zgcdn (S n) a b) -> Zgcdn n a b <> Zgcdn (S n) a b -> fibonacci (S n) <= a /\ fibonacci (S (S n)) <= b.
proof: Proof. intros n; induction n as [|n IHn]. - intros [|a|a]; intros; simpl; lia. - intros [|a|a] b (Ha,Ha'); [simpl; lia | | easy ]. remember (S n) as m eqn:Heqm. rewrite Heqm at 2. simpl Zgcdn. unfold Z.modulo; generalize (Z_div_mod b (Zpos a) eq_refl). destruct (Z.div_eucl b (Zpos a)) as (q,r). intros (EQ,(Hr,Hr')). Z.le_elim Hr. + replace (fibonacci (S (S m))) with (fibonacci (S m) + fibonacci m) by auto. intros. destruct (IHn r (Zpos a) (conj Hr Hr')); auto. * assert (EQ' : r = Zpos a * (-q) + b) by (rewrite EQ; ring). rewrite EQ' at 1. apply Zis_gcd_sym. apply Zis_gcd_for_euclid2; auto. apply Zis_gcd_sym; auto. * split. -- auto. -- destruct q. 1:lia. 1-2: nia. + clear IHn EQ Hr'; intros _. subst r; simpl; rewrite Heqm. destruct n. * simpl. lia. * now destruct 1. Qed.
imports: ZArith_base ZArithRing Zdiv Znumtheory Lia