proposition: Lemma fib_monotone_bis a b: fib a < fib b -> a < b.
proof: Proof. by rewrite ltnNge; case: (ltnP a b) => // /fib_monotone ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)