fact: Fixpoint f_k (n : nat) := match n with | 0 => 0 | n.+1 => let k0 := f_k n in if n.+1 < a k0.+1 then k0 else k0.+1 end.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp tactics floor arithmetics multinomial