proposition: Lemma natsummationswap { R : commring } ( upper : nat ) ( f : nat -> nat -> R ) : natsummation0 upper ( fun i : nat => natsummation0 i (fun j : nat => f j ( sub i j ) ) ) = natsummation0 upper ( fun k : nat => natsummation0 ( sub upper k ) ( fun l : nat => f k l ) ).
proof: Proof. revert f. induction upper. - auto. - intros f. change ( natsummation0 upper (fun i : nat => natsummation0 i (fun j : nat => f j ( sub i j ))) + natsummation0 ( S upper ) ( fun j : nat => f j ( sub ( S upper ) j ) ) = natsummation0 upper (fun k : nat => natsummation0 (S upper - k) (fun l : nat => f k l)) + natsummation0 ( sub ( S upper ) ( S upper ) ) ( fun l : nat => f ( S upper ) l ) ). change ( natsummation0 upper (fun i : nat => natsummation0 i (fun j : nat => f j ( sub i j))) + ( natsummation0 upper ( fun j : nat => f j ( sub ( S upper ) j ) ) + f ( S upper ) ( sub ( S upper ) ( S upper ) ) ) = natsummation0 upper (fun k : nat => natsummation0 (S upper - k) (fun l : nat => f k l)) + natsummation0 ( sub ( S upper ) ( S upper ) ) ( fun l : nat => f ( S upper ) l ) ). assert ( natsummation0 upper (fun k : nat => natsummation0 ( S ( sub upper k ) ) (fun l : nat => f k l)) = natsummation0 upper (fun k : nat => natsummation0 (sub ( S upper ) k) (fun l : nat => f k l)) ) as A. { apply natsummationpathsupperfixed. intros n q. apply natsummationsswapminus. exact q. } rewrite <- A. change ( fun k : nat => natsummation0 (S ( sub upper k)) (fun l : nat => f k l) ) with ( fun k : nat => natsummation0 ( sub upper k ) ( fun l : nat => f k l ) + f k ( S ( sub upper k ) ) ). rewrite ( natsummationplusdistr upper _ ( fun k : nat => f k ( S ( sub upper k ) ) ) ). rewrite IHupper. rewrite minusnn0. rewrite ( ringassoc1 R). assert ( natsummation0 upper ( fun j : nat => f j ( sub ( S upper ) j ) ) = natsummation0 upper ( fun k : nat => f k ( S ( sub upper k ) ) ) ) as g. { apply natsummationpathsupperfixed. intros m q. rewrite pathssminus. + apply idpath. + apply ( natlehlthtrans _ upper ). * assumption. * apply natlthnsn. } rewrite g. apply idpath. Defined.
imports: UniMath.PAdics.lemmas UniMath.Algebra.RigsAndRings UniMath.NumberSystems.Integers