proposition: Lemma fib_eq1 n: (fib n == 1) = ((n == 1) || (n == 2)).
proof: Proof. case:n => [|[|[|n]]] //;case: eqP => // Hm; have: 1 < 2 < n.+3 by []. by move/fib_smonotone; rewrite Hm. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)