Lemma leadingcoefficientapartdec ( R : aintdom ) ( a : fpscommring R ) ( is : isacommringapartdec R ) ( p : a 0%nat # 0 ) : forall n : nat, forall b : fpscommring R, ( b n # 0 ) -> acommringapartrel ( acommringfps R ) ( a * b ) 0. Proof. intros n. induction n. - intros b q. intros P s. apply s. split with 0%nat. change ( ( a * b ) 0%nat ) with ( ( a 0%nat ) * ( b 0%nat ) ). apply R; assumption. - intros b q. destruct ( is ( b 0%nat ) 0 ) as [ left | right ]. + intros P s. apply s. split with 0%nat. change ( ( a * b ) 0%nat ) with ( ( a 0%nat ) * ( b 0%nat ) ). apply R; assumption. + assert ( acommringapartrel ( acommringfps R ) ( a * ( fpsshift b ) ) 0 ) as j. { apply IHn. unfold fpsshift. assumption. } use (hinhuniv _ j). intro k. destruct k as [ k i ]. intros P s. apply s. rewrite <- ( fpsshiftandmult a b right k ) in i. split with ( S k ). assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.