proposition: Lemma nf_tail_lt_nf b b': lt b' b -> nf b' -> forall a n, nf (cons a n b) -> nf (cons a n b').
proof: Proof. intros H H0 a n H1; destruct b. - destruct (not_lt_zero H). - destruct b'. + do 2 auto_nf. + destruct (lt_inv H). * apply cons_nf; trivial. -- apply lt_trans with b1; auto. eapply nf_inv3; eauto. -- eapply nf_inv1; eauto. * destruct H2 as [H2 | H2]; decompose [and] H2; subst. 2: clear H2; apply cons_nf; auto. -- apply cons_nf; auto. eapply nf_inv3; eauto. eapply nf_inv1; eauto. -- eapply nf_inv3; eauto. -- eapply nf_inv1; eauto. 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)