proposition: Lemma fib_monotone m n: m <= n -> fib m <= fib n.
proof: Proof. elim: n=> [|[|n] IH]; first by case: m. by case: m{IH}=> [|[]]. rewrite fibSS leq_eqVlt; case/orP=>[|Hm]; first by move/eqP->. apply: (leq_trans (IH Hm)); exact: leq_addr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)