proposition: Lemma bv_add_neg_unit: forall a, bv_add a (bv_not a) = mk_list_true (nat_of_N (size a)).
proof: Proof. intro a. unfold bv_add, bv_not, size, bits. rewrite not_list_length. rewrite N.eqb_compare. rewrite N.compare_refl. unfold add_list. rewrite add_neg_list_carry_neg_f. rewrite Nat2N.id, not_list_length. reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance