proposition: Lemma L8 n c p : alpha = FS n -> beta = cons c p zero -> c <> zero -> P beta.
proof: Proof. intros; subst; intros. assert (nf (FS n * cons c p zero)). { rewrite L7; auto; split; auto. } split; auto. intros _ gamma H3; assert (nf gamma) by eauto with T1. destruct (cases_for_mult H2). - subst;rewrite mult_a_0; auto. rewrite L7; auto. - destruct H4. + destruct H4; subst; rewrite mult_compat. rewrite L7; auto. * apply LT2; eauto with T1. -- apply not_zero_lt; eauto with T1. + destruct H4. * destruct H4 as [a [q [H6 H7]]]; subst; rewrite L7; auto. -- rewrite L7; auto. * destruct H4 as [a [q [b [H6 [H7 H8]]]]]; subst. rewrite L6; auto. rewrite L6; auto. -- rewrite mult_a_0. destruct (LT_inv H3). ++ apply LT2; auto. rewrite <- L6; auto. ** destruct (@IHbeta (cons a q b)); auto with T1. ++ destruct H4. subst; destruct H5. ** apply LT3; auto with T1. rewrite <- L6 ; auto. destruct (@IHbeta (cons c q b)); auto. ** destruct H4. destruct (not_LT_zero H5); auto. 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)