proposition: Lemma nf_tail_lt alpha n beta gamma : nf (cons alpha n beta) -> gamma t1< beta -> nf (cons alpha n gamma).
proof: Proof. destruct beta. - intros H H0; destruct (not_LT_zero H0). - intros H H0; destruct gamma. + apply single_nf; eapply nf_inv1; eauto. + destruct (LT_inv_strong H0). * apply cons_nf. -- specialize (nf_inv3 H); intros H2; destruct H1 as [H3 [H4 H5]]. apply lt_trans with beta1; auto. -- eapply nf_inv1; eauto. -- destruct H0 as [H2 [H3 H4]]; auto. * subst; apply nf_cons_LT. -- repeat split. ++ eapply nf_inv1; eapply nf_inv2; eauto. ++ eapply nf_inv3; eauto. ++ eapply nf_inv1; eauto. -- eapply nf_inv1; eauto. -- destruct H0; tauto. * subst; apply nf_cons_LT. -- repeat split. ++ eapply nf_inv1; eapply nf_inv2; eauto. ++ eapply nf_inv3; eauto. ++ eapply nf_inv1; eauto. -- eapply nf_inv1; eauto. -- destruct H0; tauto. 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)