Lemma fpsshiftandmult { R : commring } ( a b : fpscommring R ) ( p : b 0%nat = 0 ) : forall n : nat, ( a * b ) ( S n ) = ( a * ( fpsshift b ) ) n. Proof. intros. induction n. - change ( a * b ) with ( fpstimes R a b ). change ( a * fpsshift b ) with ( fpstimes R a ( fpsshift b ) ). unfold fpstimes. unfold fpsshift. simpl. rewrite p. rewrite ( ringmultx0 R ). rewrite ( ringrunax1 R ). apply idpath. - change ( a * b ) with ( fpstimes R a b ). change ( a * fpsshift b ) with ( fpstimes R a ( fpsshift b ) ). unfold fpsshift. unfold fpstimes. change ( natsummation0 (S (S n)) (fun x : nat => a x * b (sub ( S (S n) ) x)) ) with ( natsummation0 ( S n ) ( fun x : nat => a x * b ( sub ( S ( S n ) ) x ) ) + a ( S ( S n ) ) * b ( sub ( S ( S n ) ) ( S ( S n ) ) ) ). rewrite minusnn0. rewrite p. rewrite ( ringmultx0 R ). rewrite ringrunax1. apply natsummationpathsupperfixed. intros x j. apply maponpaths. apply maponpaths. rewrite pathssminus. + apply idpath. + apply ( natlehlthtrans _ ( S n ) _ ). * assumption. * apply natlthnsn. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.