equal
deleted
inserted
replaced
8 |
8 |
9 text {* Auxiliary. *} |
9 text {* Auxiliary. *} |
10 |
10 |
11 lemma add_setsum_orient: |
11 lemma add_setsum_orient: |
12 "setsum f {k..<j} + setsum f {l..<k} = setsum f {l..<k} + setsum f {k..<j}" |
12 "setsum f {k..<j} + setsum f {l..<k} = setsum f {l..<k} + setsum f {k..<j}" |
13 by (fact plus.commute) |
13 by (fact add.commute) |
14 |
14 |
15 lemma add_setsum_int: |
15 lemma add_setsum_int: |
16 fixes j k l :: int |
16 fixes j k l :: int |
17 shows "j < k \<Longrightarrow> k < l \<Longrightarrow> setsum f {j..<k} + setsum f {k..<l} = setsum f {j..<l}" |
17 shows "j < k \<Longrightarrow> k < l \<Longrightarrow> setsum f {j..<k} + setsum f {k..<l} = setsum f {j..<l}" |
18 by (simp_all add: setsum_Un_Int [symmetric] ivl_disj_un) |
18 by (simp_all add: setsum_Un_Int [symmetric] ivl_disj_un) |