proposition: Theorem summation_aux_rtl : ∀ g b len, (summation_aux r b len g = summation_aux r b len (λ i, g (b + len - 1 + b - i)%nat))%K.
proof: Proof. intros g b len. revert g b. induction len; intros; [ reflexivity | idtac ]. remember (S len) as x. rewrite Heqx in |- * at 1. simpl; subst x. rewrite IHlen. rewrite summation_aux_succ_last. rewrite Nat.add_succ_l, Nat_sub_succ_1. do 2 rewrite Nat.add_succ_r; rewrite Nat_sub_succ_1. rewrite Nat.add_sub_swap, Nat.sub_diag; auto. rewrite rng_add_comm. apply rng_add_compat_r, summation_aux_compat. intros; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2