Lemma hzfpstimeswhenzero ( a : fpscommring hz ) ( m k : nat ) ( is : ( forall m : nat, natlth m k -> a m = 0%hz ) ) : forall b : fpscommring hz, forall k' : nat, forall is' : ( forall m : nat, natlth m k' -> b m = 0%hz ) , natlth m ( k + k' )%nat -> ( a * b ) m = 0%hz. Proof. revert k is. induction m. - intros k. intros is b k' is' j. change ( a 0%nat * b 0%nat = 0%hz ). destruct k. + rewrite ( is' 0%nat j ). rewrite hzmultx0. apply idpath. + assert ( natlth 0 ( S k ) ) as i. { apply ( natlehlthtrans _ k _ ). * apply natleh0n. * apply natlthnsn. } rewrite ( is 0%nat i ). rewrite hzmult0x. apply idpath. - intros k is b k' is' j. change ( natsummation0 ( S m ) ( fun x : nat => a x * b ( sub ( S m ) x ) ) = 0%hz ). change ( natsummation0 m ( fun x : nat => a x * b ( sub ( S m ) x ) ) + a ( S m ) * b ( sub ( S m ) ( S m ) ) = 0%hz ). assert ( a ( S m ) * b ( sub ( S m ) ( S m ) ) = 0%hz ) as g. { destruct k. + destruct k'. * apply fromempty. apply ( negnatgth0n ( S m ) j ). * rewrite minusnn0. rewrite ( is' 0%nat ( natlehlthtrans 0%nat k' ( S k' ) ( natleh0n k' ) ( natlthnsn k' ) ) ). rewrite hzmultx0. apply idpath. + destruct k'. * rewrite natplusr0 in j. rewrite ( is ( S m ) j ). rewrite hzmult0x. apply idpath. * rewrite minusnn0. rewrite ( is' 0%nat ( natlehlthtrans 0%nat k' ( S k' ) ( natleh0n k' ) ( natlthnsn k' ) ) ). rewrite hzmultx0. apply idpath. } rewrite g. rewrite hzplusr0. set ( b' := fpsshift b ). assert ( natsummation0 m ( fun x : nat => a x * b ( sub ( S m ) x ) ) = natsummation0 m ( fun x : nat => a x * b' ( sub m x ) ) ) as f. { apply natsummationpathsupperfixed. intros n i. unfold b'. unfold fpsshift. rewrite pathssminus. + apply idpath. + apply ( natlehlthtrans _ m _ ). * assumption. * apply natlthnsn. } rewrite f. change ( ( a * b' ) m = 0%hz ). assert ( natlth m ( k + k' ) ) as one. { apply ( istransnatlth _ ( S m ) _ ). + apply natlthnsn. + assumption. } destruct k'. + assert ( forall m : nat, natlth m 0%nat -> b' m = 0%hz ) as two. { intros m0 j0. apply fromempty. apply ( negnatgth0n m0). assumption. } apply ( IHm k is b' 0%nat two one ). + assert ( forall m : nat, natlth m k' -> b' m = 0%hz ) as two. { intros m0 j0. change ( b ( S m0 ) = 0%hz ). apply is'. assumption. } assert ( natlth m ( k + k' )%nat ) as three. { rewrite natplusnsm in j. apply j. } apply ( IHm k is b' k' two three ). 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.