proposition: Theorem summation_rtl : ∀ g b k, (Σ (i = b, k), g i = Σ (i = b, k), g (k + b - i)%nat)%K.
proof: Proof. intros g b k. unfold summation. rewrite summation_aux_rtl. apply summation_aux_compat; intros i (Hi, Hikb). destruct b; simpl. rewrite Nat.sub_0_r; reflexivity. rewrite Nat.sub_0_r. simpl in Hikb. eapply Nat.le_lt_trans in Hikb; eauto . apply lt_O_minus_lt, Nat.lt_le_incl in Hikb. remember (b + (k - b))%nat as x eqn:H . rewrite Nat.add_sub_assoc in H; auto. rewrite Nat.add_sub_swap in H; auto. rewrite Nat.sub_diag in H; subst x; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2