proposition: Lemma bv_add_assoc : forall n (a b c :bitvector n), bv_eq (bv_add a (bv_add b c)) (bv_add (bv_add a b) c) = true.
proof: Proof. intros n a b c. unfold bv_eq. rewrite M.bv_eq_reflect. simpl. apply (@M.bv_add_assoc n a b c); now rewrite wf. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance