proposition: Lemma n_between_a n (Hn : (2 <= n)) : (a (f_k n) <= n < a ((f_k n).+1)).
proof: Proof. elim: n Hn => // n; set k0 := f_k n => ihn. rewrite leq_eqVlt => /predU1P[<- //|]. have -> : f_k n.+1 = if n.+1 < a k0.+1 then k0 else k0.+1 by []. rewrite ltnS; move/ihn. case: ifP; first by move -> => /andP [Hn _]; rewrite ltnW. move => Hf /andP [H1 H2]. by rewrite leq_eqVlt Hf orbF in H2; move /eqP: H2 => ->; rewrite a_grows1 leqnn. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial