[STATEMENT]
lemma test_bit_rcat:
  "sw = size (hd wl) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> bit rc n =
    (n < size rc \<and> n div sw < size wl \<and> bit ((rev wl) ! (n div sw)) (n mod sw))"
  for wl :: "'a::len word list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sw = size (hd wl); rc = word_rcat wl\<rbrakk> \<Longrightarrow> bit rc n = (n < size rc \<and> n div sw < length wl \<and> bit (rev wl ! (n div sw)) (n mod sw))
[PROOF STEP]
by (simp add: word_size word_rcat_def rev_map bit_horner_sum_uint_exp_iff bit_simps not_le)