equal
deleted
inserted
replaced
1100 apply (clarsimp simp: Let_def split: ls_splits) |
1100 apply (clarsimp simp: Let_def split: ls_splits) |
1101 apply (erule thin_rl) |
1101 apply (erule thin_rl) |
1102 apply (case_tac m) |
1102 apply (case_tac m) |
1103 apply simp |
1103 apply simp |
1104 apply (case_tac "m <= n") |
1104 apply (case_tac "m <= n") |
1105 apply (auto simp add: div_add_self2) |
1105 apply auto |
1106 done |
1106 done |
1107 |
1107 |
1108 lemma bin_rsplit_len: |
1108 lemma bin_rsplit_len: |
1109 "n\<noteq>0 ==> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n" |
1109 "n\<noteq>0 ==> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n" |
1110 unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len) |
1110 unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len) |