proposition: Lemma fibonacci_incr : forall n m, (n<=m)%nat -> fibonacci n <= fibonacci m.
proof: Proof. induction 1 as [|m H IH]. - auto with zarith. - apply Z.le_trans with (fibonacci m); auto. clear. destruct m as [|m]. + simpl; auto with zarith. + change (fibonacci (S m) <= fibonacci (S m)+fibonacci m). generalize (fibonacci_pos m); lia. Qed.
imports: ZArith_base ZArithRing Zdiv Znumtheory Lia