proposition: Lemma bv_add_assoc: forall n a b c, (size a) = n -> (size b) = n -> (size c) = n -> (bv_add a (bv_add b c)) = (bv_add (bv_add a b) c).
proof: Proof. intros n a b c H0 H1 H2. unfold bv_add, size, bits in *. rewrite H1, H2. rewrite N.eqb_compare. rewrite N.eqb_compare. rewrite N.compare_refl. rewrite <- (@length_add_list_eq b c). rewrite H0, H1. rewrite N.compare_refl. rewrite N.eqb_compare. rewrite N.eqb_compare. rewrite N.compare_refl. rewrite <- (@length_add_list_eq a b). rewrite H0. rewrite N.compare_refl. rewrite add_list_assoc. reflexivity. now rewrite <- Nat2N.inj_iff, H0. now rewrite <- Nat2N.inj_iff, H1. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance