proposition: Theorem summation_only_one : ∀ g n, (Σ (i = n, n), g i = g n)%K.
proof: Proof. intros g n. unfold summation. rewrite Nat.sub_succ_l; [ idtac | reflexivity ]. rewrite Nat.sub_diag; simpl. rewrite rng_add_0_r; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2