[STATEMENT]
lemma cbox_translation: "cbox (c + a) (c + b) = image (\<lambda>x. c + x) (cbox a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cbox (c + a) (c + b) = (+) c ` cbox a b
[PROOF STEP]
using image_affinity_cbox [of 1 c a b]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. 1 *\<^sub>R x + c) ` cbox a b = (if cbox a b = {} then {} else if 0 \<le> 1 then cbox (1 *\<^sub>R a + c) (1 *\<^sub>R b + c) else cbox (1 *\<^sub>R b + c) (1 *\<^sub>R a + c))

goal (1 subgoal):
 1. cbox (c + a) (c + b) = (+) c ` cbox a b
[PROOF STEP]
using box_ne_empty [of "a+c" "b+c"]  box_ne_empty [of a b]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. 1 *\<^sub>R x + c) ` cbox a b = (if cbox a b = {} then {} else if 0 \<le> 1 then cbox (1 *\<^sub>R a + c) (1 *\<^sub>R b + c) else cbox (1 *\<^sub>R b + c) (1 *\<^sub>R a + c))
(cbox (a + c) (b + c) \<noteq> {}) = (\<forall>i\<in>Basis. (a + c) \<bullet> i \<le> (b + c) \<bullet> i)
(box (a + c) (b + c) \<noteq> {}) = (\<forall>i\<in>Basis. (a + c) \<bullet> i < (b + c) \<bullet> i)
(cbox a b \<noteq> {}) = (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)
(box a b \<noteq> {}) = (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)

goal (1 subgoal):
 1. cbox (c + a) (c + b) = (+) c ` cbox a b
[PROOF STEP]
by (auto simp: inner_left_distrib add.commute)