fact: Definition extension (n : nat) (p : forall k : nat, k < n -> nat) k := match lt_dec k n with | left x => p k x | _ => 0 end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)