proposition: Remark R4_3_4 : (canon beta (S n1) t1<= canon alpha (S n2))%t1.
proof: Proof. destruct (T1_eq_dec alpha beta). - subst. clear H4 H0; induction H1. + apply LE_refl. now apply nf_canon. + apply LE_trans with (canon beta (S m)); auto. apply canonS_LE; auto. - assert (beta t1< alpha)%t1. { apply const_pathS_eps_LE_2 in H4;auto. destruct H4, H2. do 2 (split; auto). destruct H2; auto. now destruct n. } assert (const_pathS n2 alpha (canon beta (S n1))). { generalize R4_3_3; inversion 1. auto. subst. destruct (@LT_irrefl beta). apply LT_trans with (canon beta (S n1)); auto. apply canonS_LT ;auto. intro;subst; cbn in H00; now destruct H00. } inversion H2. subst; destruct H3 as [_ H3]. rewrite H3; apply LE_refl. apply nf_canon;auto. destruct H3 as [_ H3]. subst y; eapply const_pathS_LE; eauto. eapply nf_canon;eauto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)