proposition: Lemma invBCons n b (p: BITS n) : invB (cons_tuple b p) = cons_tuple (negb b) (invB p).
proof: Proof. rewrite /invB. by rewrite liftUnOpCons. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations mathcomp(ssralg)