proposition: Lemma fibonacci_pos : forall n, 0 <= fibonacci n.
proof: Proof. enough (forall N n, (n<N)%nat -> 0<=fibonacci n) by eauto. intros N; induction N as [|N IHN]. - intros; lia. - intros [ | [ | n ] ]. 1-2: simpl; lia. intros. change (0 <= fibonacci (S n) + fibonacci n). generalize (IHN n) (IHN (S n)); lia. Qed.
imports: ZArith_base ZArithRing Zdiv Znumtheory Lia