proposition: Lemma addNB n (p: BITS n) : addB p (negB p) = #0.
proof: Proof. by rewrite addBC addBN. 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)