proposition: Lemma standard_path_LE : forall j beta i alpha, standard_path i alpha j beta -> (i <= j)%nat.
proof: Proof. eapply standard_path_to_le_inv; eauto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)