[STATEMENT]
lemma iT_Div_cut_ge2: "
  0 < k \<Longrightarrow> (I \<oslash> k) \<down>\<ge> (t div k) = I \<down>\<ge> (t - t mod k) \<oslash> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k \<Longrightarrow> (I \<oslash> k) \<down>\<ge> (t div k) = I \<down>\<ge> (t - t mod k) \<oslash> k
[PROOF STEP]
by (frule iT_Div_cut_ge[of k I "t div k"], simp add: div_mult_cancel)