fact: Fixpoint decode_rec (v q r : nat) {struct q} := match q, r with | 0, _ => [:: v] | q'.+1, 0 => v :: [rec 0, q', q'] | q'.+1, 1 => [rec v.+1, q', q'] | q'.+1, r'.+2 => [rec v, q', r'] end where "[ 'rec' v , q , r ]" := (decode_rec v q r).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)