proposition: Lemma fib_smonotone : forall m n, 1 < m < n -> fib m < fib n.
proof: Proof. move=> m n; elim: n=> [|[|n] IH]; first by rewrite andbF. by rewrite ltnNge leq_eqVlt orbC andbC; case: leq. rewrite fibSS andbC; case/andP; rewrite leq_eqVlt; case/orP. by rewrite eqSS; move/eqP=> -> H1m; rewrite -addn1 leq_add // fib_gt0. by move=> H1m H2m; apply: ltn_addr; apply: IH; rewrite // H2m. Qed.
imports: mathcomp(all_ssreflect all_algebra)