proposition: Corollary negB_fromNat n m : m < 2^n -> negB (n:=n) #m = #(2^n - m).
proof: Proof. apply negB_or_invB_fromNat. 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)