proposition: Lemma L4 : forall a n b p, a <> zero -> alpha = cons a n b -> beta = FS p -> P beta.
proof: Proof. unfold P; intros; subst; split. - simpl; destruct a. + now destruct H. + apply nf_coeff_irrelevance with n; auto. - intros _ gamma H4; destruct (LT_of_finite H4). + subst; rewrite mult_a_0; simpl; destruct a. * apply LT1. apply nf_of_finite in Halpha. now destruct H. * auto with T1. + destruct H0 as [p0 [H5 H6]]; subst; simpl. assert (p0 + n * S p0 < p + n * S p)%nat. { apply Nat.add_lt_le_mono; auto. apply PeanoNat.Nat.mul_le_mono_l; abstract lia. } destruct a. * apply LT3;auto. * apply LT3; eauto with T1. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)