proposition: Corollary Cor12 (alpha : T1) : nf alpha -> forall beta i n, beta t1< alpha -> i < n -> const_path (S i) alpha beta -> const_path (S n) alpha beta.
proof: Proof. transfinite_induction_lt alpha. clear alpha ; intros alpha Hrec Halpha; intros. destruct (zero_limit_succ_dec Halpha). - destruct s. + subst; destruct (not_LT_zero H). + destruct H1. { destruct H1 as [H1 e]; subst y. assert (H2: const_pathS 0 (canon alpha (S n)) (canon alpha (S i))). { apply KS_thm_2_4; auto. } constructor 2 with (canon alpha (S n)). - split ; auto. - apply Hrec with 0; auto. + apply nf_canon; auto. + apply canon_lt; auto. + apply nf_canon; auto. + apply canonS_limit_mono; auto. + apply Nat.le_lt_trans with i; auto with arith. } { destruct H1 as [H01 H1]; subst y; assert (const_path (S n) (canon alpha (S i)) z). { apply Hrec with i;auto. apply nf_canon; auto. apply canon_lt;auto. apply nf_canon; auto. eapply const_pathS_LT. apply nf_canon; auto. eapply H2. } { red. red. rewrite <- clos_trans_t1n_iff. apply t_trans with (canon alpha (S n)). left. auto. right with (canon alpha (S i)). rewrite clos_trans_t1n_iff. apply Hrec with 0;eauto. now apply nf_canon. apply canon_lt; auto. apply nf_canon; auto. apply canonS_limit_mono ;auto. apply Nat.le_lt_trans with i;auto. auto with arith. apply KS_thm_2_4; auto. now rewrite clos_trans_t1n_iff. } } - destruct s as [x [H2 H3]]; subst alpha. { destruct H1. - destruct H1 as [H01 H1] . subst y. rewrite canon_succ. left. rewrite canon_succ;auto. auto. - destruct H1 as [H01 H1]; subst y; rewrite canon_succ in H3. right with x. + rewrite canon_succ;auto. + destruct (T1_eq_dec x zero). { subst x; auto. assert (z = zero). { simpl succ in H; apply LT_one in H; auto. } constructor 1. subst. split; auto. inversion_clear H3. now destruct H1. now destruct H1. } apply Hrec with i;eauto. apply lt_succ. eapply const_pathS_LT;eauto. + auto. } Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)