proposition: 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: 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.
imports: UniMath.PAdics.lemmas UniMath.Algebra.RigsAndRings UniMath.NumberSystems.Integers