proposition: Corollary LT_to_standard_path (alpha beta : T1) : beta t1< alpha -> {n : nat & {j:nat | standard_path (S n) alpha j beta}}.
proof: Proof. intros H; assert (nf alpha) by eauto with T1. destruct (Lemma2_6_1 H0 H) as [n Hn]. exists n; apply constant_to_standard_path; auto. apply LE_LT_trans with beta; eauto with T1. apply LE_zero; eauto with T1. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)