proposition: Lemma standard_path_to_le_inv : forall j beta i alpha, standard_path_to j beta i alpha -> (i <= j)%nat.
proof: Proof. induction 1. - subst;auto with arith. - auto with arith. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)