proposition: Lemma bv_shr_size n a b : size a = n -> size b = n -> size (bv_shr a b) = n.
proof: Proof. unfold bv_shr. intros H1 H2. rewrite H1, H2. rewrite N.eqb_compare. rewrite N.compare_refl. unfold size in *. rewrite <- (@length_shr_be a b (nat_of_N n)). now rewrite N2Nat.id. now apply (f_equal (N.to_nat)) in H1; rewrite Nat2N.id in H1. now apply (f_equal (N.to_nat)) in H2; rewrite Nat2N.id in H2. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance