Lemma natsummationsswapminus { R : commring } { upper n : nat } ( f : nat -> R ) ( q : natleh n upper ) : natsummation0 ( S ( sub upper n ) ) f = natsummation0 ( sub ( S upper ) n ) f. Proof. revert n f q. induction upper. - intros n f q. destruct n. + auto. + apply fromempty. exact ( negnatlehsn0 n q ). - intros n f q. destruct n. + auto. + change ( natsummation0 ( S ( sub upper n ) ) f = natsummation0 ( sub ( S upper ) n ) f ). apply IHupper. apply q. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.