proposition: Lemma lnot_repr: forall i bs, native_repr i bs -> native_repr (lnot i) (invB bs).
proof: Proof. move=> i ?. rewrite /native_repr eq_adj. move/eqP=> <-. apply/eqInt16P. move: i; apply/forallInt16P; last by apply lnot_valid. move=> i; apply/eqInt16P. Qed.
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits)