proposition: Lemma Lemma_4_5_1 n alpha: nf alpha -> forall s t , ptwise_le s t -> sorted_ge n s -> sorted_ge n t -> const_pathS_eps (simple_last n t) (gnawS alpha t) (gnawS alpha s).
proof: Proof. intros Halpha s t H; unfold ptwise_le in H. pattern s , t; eapply Forall2_indR with Peano.le; eauto. - intros; cbn; now right. - intros; subst; repeat rewrite gnawS_app. replace (simple_last n (l' ++ y :: nil)) with y. assert (const_pathS_eps y (gnawS alpha l') (gnawS alpha l)). { eapply Cor12_2 with (simple_last n l'); eauto. eapply gnawS_nf; auto. eapply sorted_cut;eauto. eapply H1. all : eapply sorted_ge_prefix; eauto. } eapply Lemma_4_3 with (simple_last n l'); auto. eapply gnawS_nf; eauto. eapply gnawS_nf; eauto. eapply sorted_cut;eauto. eapply H1. eapply sorted_ge_prefix; eauto. eapply sorted_ge_prefix; eauto. now rewrite simple_last_app1. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)