proposition: Theorem summation_compat : ∀ g h b k, (∀ i, b ≤ i ≤ k → (g i = h i)%K) → (Σ (i = b, k), g i = Σ (i = b, k), h i)%K.
proof: Proof. intros g h b k Hgh. apply summation_aux_compat. intros i (_, Hi). apply Hgh. split; [ apply Nat.le_add_r | idtac ]. apply Nat.lt_add_lt_sub_r, le_S_n in Hi. rewrite Nat.add_comm; assumption. Qed.
imports: Utf8 QArith NPeano Misc Field2