proposition: Lemma pos_of_bitseq_rev : forall y p, rev (bitseq_of_pos p) = true :: y -> pos_of_bitseq (rev y) = p.
proof: Proof. elim/last_ind => [p Hp /=|h t IH []// p /=]. apply/esym/bitseq_of_pos_true; by rewrite -[LHS]revK Hp. - rewrite rev_cons -rcons_cons => /eqP. rewrite eqseq_rcons => /andP[/eqP/IH H1 /eqP <-]. by rewrite rev_rcons /= H1. - rewrite rev_cons -rcons_cons => /eqP. rewrite eqseq_rcons => /andP[/eqP/IH H1 /eqP <-]. by rewrite rev_rcons /= H1. - by move: p; case => <-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext