proposition: Lemma bv_add_empty_neutral_l: forall a, (bv_add (mk_list_false (length (bits a))) a) = a.
proof: Proof. intro a. unfold bv_add, size, bits. rewrite N.eqb_compare. rewrite length_mk_list_false. rewrite N.compare_refl. rewrite add_list_empty_neutral_l. reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance