proposition: Lemma Proposition_2_3a: forall n alpha , nf alpha -> alpha <> zero -> forall beta gamma, LT gamma beta -> const_pathS n alpha gamma -> const_pathS n alpha beta -> const_pathS n beta gamma.
proof: Proof. intros n alpha; transfinite_induction alpha. clear alpha ; intros alpha Hrec H H' beta gamma H0 H1 H2. destruct (const_pathS_inv H1), (const_pathS_inv H2). - subst; destruct (LT_irrefl H0). - destruct (T1_eq_dec alpha zero). + now destruct H'. + subst gamma; assert False. { apply const_pathS_LE in H4. destruct (@LT_irrefl beta). eapply LE_LT_trans;eauto. apply nf_canon;auto. } contradiction. - subst beta; auto. - destruct (T1_eq_dec alpha zero). + subst alpha. destruct (const_pathS_zero H2). + apply (Hrec (canon alpha (S n))); auto. apply canonS_LT; auto. apply nf_canon;auto. intro H5;rewrite H5 in H4. inversion_clear H4; destruct H6; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)