proposition: Theorem summation_aux_compat : ∀ g h b₁ b₂ len, (∀ i, 0 ≤ i < len → (g (b₁ + i)%nat = h (b₂ + i)%nat)%K) → (summation_aux r b₁ len g = summation_aux r b₂ len h)%K.
proof: Proof. intros g h b₁ b₂ len Hgh. revert b₁ b₂ Hgh. induction len; intros; [ reflexivity | simpl ]. rewrite IHlen. apply rng_add_compat_r. assert (0 ≤ 0 < S len) as H. split; [ reflexivity | apply Nat.lt_0_succ ]. apply Hgh in H. do 2 rewrite Nat.add_0_r in H; assumption. intros i Hi. do 2 rewrite Nat.add_succ_l, <- Nat.add_succ_r. apply Hgh. split; [ apply Nat.le_0_l | idtac ]. apply lt_n_S. destruct Hi; assumption. Qed.
imports: Utf8 QArith NPeano Misc Field2