proposition: Lemma Zgcd_bound_fibonacci : forall a, 0 < a -> a < fibonacci (Zgcd_bound a).
proof: Proof. intros a; destruct a as [|p|p]; [lia| | intro H; discriminate]. intros _. induction p as [p IHp|p IHp|]; [ | | compute; auto ]; simpl Zgcd_bound in *; rewrite Nat.add_comm; simpl plus; set (n:= (Pos.size_nat p+Pos.size_nat p)%nat) in *; simpl; assert (n <> O) as H by (unfold n; destruct p; simpl; auto). - destruct n as [ |m]; [elim H; auto| ]. generalize (fibonacci_pos m); rewrite Pos2Z.inj_xI; lia. - destruct n as [ |m]; [elim H; auto| ]. generalize (fibonacci_pos m); rewrite Pos2Z.inj_xO; lia. Qed.
imports: ZArith_base ZArithRing Zdiv Znumtheory Lia