[STATEMENT]
lemma aux_lt_implies_mask:
  assumes "a < 2^k"
  shows "\<forall>r\<ge>k. a \<exclamdown> r = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r\<ge>k. a \<exclamdown> r = 0
[PROOF STEP]
using nth_bit_def assms
[PROOF STATE]
proof (prove)
using this:
?num \<exclamdown> ?k = ?num div 2 ^ ?k mod 2
a < 2 ^ k

goal (1 subgoal):
 1. \<forall>r\<ge>k. a \<exclamdown> r = 0
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>\<And>num k. num \<exclamdown> k = num div 2 ^ k mod 2; a < 2 ^ k; k \<le> r\<rbrakk> \<Longrightarrow> a div 2 ^ r mod 2 = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>\<And>num k. num \<exclamdown> k = num div 2 ^ k mod 2; a < 2 ^ k; k \<le> r\<rbrakk> \<Longrightarrow> a div 2 ^ r mod 2 = 0
[PROOF STEP]
(* found by e *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>\<And>num k. num \<exclamdown> k = num div 2 ^ k mod 2; a < 2 ^ k; k \<le> r\<rbrakk> \<Longrightarrow> a div 2 ^ r mod 2 = 0
[PROOF STEP]
fix r :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>\<And>num k. num \<exclamdown> k = num div 2 ^ k mod 2; a < 2 ^ k; k \<le> r\<rbrakk> \<Longrightarrow> a div 2 ^ r mod 2 = 0
[PROOF STEP]
assume a1: "a < 2 ^ k"
[PROOF STATE]
proof (state)
this:
a < 2 ^ k

goal (1 subgoal):
 1. \<And>r. \<lbrakk>\<And>num k. num \<exclamdown> k = num div 2 ^ k mod 2; a < 2 ^ k; k \<le> r\<rbrakk> \<Longrightarrow> a div 2 ^ r mod 2 = 0
[PROOF STEP]
assume a2: "k \<le> r"
[PROOF STATE]
proof (state)
this:
k \<le> r

goal (1 subgoal):
 1. \<And>r. \<lbrakk>\<And>num k. num \<exclamdown> k = num div 2 ^ k mod 2; a < 2 ^ k; k \<le> r\<rbrakk> \<Longrightarrow> a div 2 ^ r mod 2 = 0
[PROOF STEP]
have "a div 2 ^ k = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a div 2 ^ k = 0
[PROOF STEP]
using a1 Euclidean_Division.div_eq_0_iff
[PROOF STATE]
proof (prove)
using this:
a < 2 ^ k
(?m div ?n = 0) = (?m < ?n \<or> ?n = 0)

goal (1 subgoal):
 1. a div 2 ^ k = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a div 2 ^ k = 0

goal (1 subgoal):
 1. \<And>r. \<lbrakk>\<And>num k. num \<exclamdown> k = num div 2 ^ k mod 2; a < 2 ^ k; k \<le> r\<rbrakk> \<Longrightarrow> a div 2 ^ r mod 2 = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a div 2 ^ k = 0
[PROOF STEP]
have "2 = (0::nat) \<or> a < 2 ^ r"
[PROOF STATE]
proof (prove)
using this:
a div 2 ^ k = 0

goal (1 subgoal):
 1. 2 = 0 \<or> a < 2 ^ r
[PROOF STEP]
using a2
[PROOF STATE]
proof (prove)
using this:
a div 2 ^ k = 0
k \<le> r

goal (1 subgoal):
 1. 2 = 0 \<or> a < 2 ^ r
[PROOF STEP]
by (metis (no_types) div_le_mono nat_zero_less_power_iff neq0_conv not_le power_diff)
[PROOF STATE]
proof (state)
this:
2 = 0 \<or> a < 2 ^ r

goal (1 subgoal):
 1. \<And>r. \<lbrakk>\<And>num k. num \<exclamdown> k = num div 2 ^ k mod 2; a < 2 ^ k; k \<le> r\<rbrakk> \<Longrightarrow> a div 2 ^ r mod 2 = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 = 0 \<or> a < 2 ^ r
[PROOF STEP]
show "a div 2 ^ r mod 2 = 0"
[PROOF STATE]
proof (prove)
using this:
2 = 0 \<or> a < 2 ^ r

goal (1 subgoal):
 1. a div 2 ^ r mod 2 = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a div 2 ^ r mod 2 = 0

goal:
No subgoals!
[PROOF STEP]
qed