proposition: Lemma bv_neg_size: forall n a, (size a) = n -> size (bv_neg a) = n.
proof: Proof. intros n a H. unfold bv_neg. unfold size, bits in *. unfold twos_complement. specialize (@add_list_carry_length_eq (map negb a) (mk_list_false (length a)) true). intros. rewrite <- H0. now rewrite map_length. rewrite map_length. now rewrite length_mk_list_false. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance