Lemma hzfpstimesnonzero ( a : fpscommring hz ) ( k : nat ) ( is : neq hz ( a k ) 0%hz × forall m : nat, natlth m k -> a m = 0%hz ) : forall k' : nat, forall b : fpscommring hz , forall is' : neq hz ( b k' ) 0%hz × forall m : nat, natlth m k' -> b m = 0%hz, ( a * b ) ( k + k' )%nat = a k * b k'. Proof. intros k'. induction k'. - intros. destruct k. + simpl. apply idpath. + rewrite natplusr0. change ( natsummation0 k ( fun x : nat => a x * b ( sub ( S k ) x ) ) + a ( S k ) * b ( sub ( S k ) ( S k ) ) = a ( S k ) * b 0%nat ). assert ( natsummation0 k ( fun x : nat => a x * b ( sub ( S k ) x ) ) = natsummation0 k ( fun x : nat => 0%hz ) ) as f. { apply natsummationpathsupperfixed. intros m i. assert ( natlth m ( S k ) ) as i0. * apply ( natlehlthtrans _ k _ ). -- assumption. -- apply natlthnsn. * rewrite ( pr2 is m i0 ). rewrite hzmult0x. apply idpath. } rewrite f. rewrite natsummationae0bottom. * rewrite hzplusl0. rewrite minusnn0. apply idpath. * intros m i. apply idpath. - intros. rewrite natplusnsm. change ( natsummation0 ( k + k' )%nat ( fun x : nat => a x * b ( sub ( S k + k' ) x ) ) + a ( S k + k' )%nat * b ( sub ( S k + k' ) ( S k + k' ) ) = a k * b ( S k' ) ). set ( b' := fpsshift b ). rewrite minusnn0. rewrite ( pr2 is' 0%nat ( natlehlthtrans 0 k' ( S k' ) ( natleh0n k' ) ( natlthnsn k' ) ) ). rewrite hzmultx0. rewrite hzplusr0. assert ( natsummation0 ( k + k' )%nat ( fun x : nat => a x * b ( sub ( S k + k' ) x ) ) = fpstimes hz a b' ( k + k' )%nat ) as f. { apply natsummationpathsupperfixed. intros m v. change ( S k + k' )%nat with ( S ( k + k' ) ). rewrite <- ( pathssminus ( k + k' )%nat m ). + apply idpath. + apply ( natlehlthtrans _ ( k + k' )%nat _ ). * assumption. * apply natlthnsn. } rewrite f. apply ( IHk' b' ). split. + apply is'. + intros m v. unfold b'. unfold fpsshift. apply is'. assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.PAdics.fps. Require Import UniMath.PAdics.frac. Require Import UniMath.PAdics.z_mod_p. Require Import UniMath.NumberSystems.Integers.