proposition: Lemma L11 n c p d : alpha = FS n -> beta = cons c p d -> c <> zero -> d <> zero -> P beta.
proof: Proof. intros H H0 H1 H2; subst alpha beta. assert (nf (FS n * cons c p d)). { rewrite L6. - assert (FS n * d t1< FS n * phi0 c). { destruct (@IHbeta (cons c 0 zero)); eauto with T1. - destruct p. + apply LT4;auto with T1. apply nf_phi0; eauto with T1. apply not_zero_lt; eauto with T1. + apply LT_trans with (cons c 0 d). * apply LT4;eauto with T1. apply not_zero_lt; eauto with T1. * apply LT3; eauto with T1 arith. - assert (H3 : FS n <> zero) by discriminate. apply (H0 H3 d). rewrite nf_LT_iff in Hbeta; tauto. } rewrite L7 in H. + rewrite nf_LT_iff; split; eauto with T1. + destruct (@IHbeta (phi0 c)). destruct p. * apply LT4;auto with T1. apply nf_phi0; eauto with T1. apply not_zero_lt; eauto with T1. * apply LT_trans with (cons c 0 d). -- apply LT4;eauto with T1. apply not_zero_lt; eauto with T1. -- apply LT3; eauto with T1 arith. * auto with arith. eauto with T1. * eauto with T1. - auto. } split; auto. intros _ gamma H4; assert (nf gamma) by eauto with T1. destruct (cases_for_mult H3). - subst; rewrite mult_a_0; auto. rewrite L6; auto. apply LT1; rewrite <- L6; auto. - destruct H5. + destruct H5; subst. rewrite mult_compat, L6; auto. apply LT2; auto. rewrite <- L6; eauto with T1. apply not_zero_lt; eauto with T1. + destruct H5. * destruct H5 as [a [q [H6 H7]]]; subst; rewrite L6; auto. rewrite L6, mult_a_0; auto. destruct (LT_inv H4); auto. -- apply LT2; auto with T1. rewrite <- L6; eauto with T1. -- destruct H5; subst. ++ destruct H7. ** apply LT3; auto with T1. rewrite <- L6; auto. ** destruct H5; subst. apply LT4; eauto with T1. rewrite <- L6; auto. apply not_zero_lt. destruct (@IHbeta d). apply tail_LT_cons; auto. eauto with T1. auto. apply L9; eauto with T1. * destruct H5 as [a [q [b [H6 [H7 H8]]]]]; subst. repeat rewrite L6; auto. destruct (LT_inv H4). -- apply LT2; auto. rewrite <- L6; auto. destruct (@IHbeta (cons a q b)); auto. rewrite <- L6; auto. -- destruct H5. subst; destruct H8. apply LT3; auto with T1. rewrite <- L6; auto. destruct (@IHbeta (cons c q b)); auto. rewrite <- L6; auto. ++ destruct H5; subst. apply LT4. rewrite <- L6; auto. destruct (@IHbeta (cons c p b)); auto. rewrite <- L6; auto. destruct (@IHbeta d); auto. apply tail_LT_cons; eauto with T1. eauto with T1. apply H9; auto. discriminate. 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)