proposition: Lemma set_pos_trecE f z e p : set_pos_trec f z e p = unzip z (set_pos f e p).
proof: Proof. by elim: p e z => [p IHp|p IHp|] [|???] [|[??]?] //=; rewrite ?IHp. Qed.
imports: HB(structures) BinPos BinNat mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq bigop)