proposition: Lemma fib_monotone : forall m n, m <= n -> fib m <= fib n.
proof: Proof. move=> m n; elim: n=> [|[|n] IH]; first by case: m. by case: {IH}m => [|[]]. rewrite fibSS leq_eqVlt; case/orP=>[|Hm]; first by move/eqP->. by apply: (leq_trans (IH _)) => //; exact: leq_addr. Qed.
imports: mathcomp(all_ssreflect all_algebra)