proposition: Lemma fib_eq1 : forall n, (fib n == 1) = ((n == 1) || (n == 2)).
proof: Proof. case=> [|[|[|n]]] //; case: eqP=> // Hm; have: 1 < 2 < n.+3 by []. by move/fib_smonotone; rewrite Hm. Qed.
imports: mathcomp(all_ssreflect all_algebra)