proposition: Lemma Fib_eq1 n: natp n -> (Fib n = \1c <-> (n = \1c \/ n = \2c)).
proof: Proof. move => nN; split; last by case => ->; rewrite ?Fib1 ?Fib2. move => eq1. case: (NleT_ell nN NS2); first by right. case /clt2; [move => ne0; move: eq1; rewrite ne0 Fib0; fprops| by left]. by move/(Fib_gt1 nN); rewrite eq1; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)