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