proposition: Lemma bv_and_nth_bitOf: forall a b n (i: nat), (size a) = n -> (size b) = n -> (i <= (nat_of_N (size a)))%nat -> nth i (bits (bv_and a b)) false = (nth i (bits a) false) && (nth i (bits b) false).
proof: Proof. intros a b n i H0 H1 H2. unfold bv_and. rewrite H0, H1. rewrite N.eqb_compare. rewrite N.compare_refl. apply map2_and_nth_bitOf; unfold size in *; unfold bits. now rewrite <- Nat2N.inj_iff, H1. rewrite Nat2N.id in H2; exact H2. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance