proposition: Lemma fib_partition a b x: fib a <= x < fib a.+1 -> fib b <= x < fib b.+1 -> a = b.
proof: Proof. move => /andP[ha hb] /andP[hc hd]; apply /eqP; rewrite eqn_leq. move: (leq_ltn_trans ha hd) => /fib_monotone_bis; rewrite ltnS => ->. by move: (leq_ltn_trans hc hb) => /fib_monotone_bis; rewrite ltnS => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)