proposition: Remark R16 : (0 < l)%nat -> const_path (n + l) alpha beta.
proof: Proof. intro H; rewrite m_def;auto. - apply Cor12_1 with n;auto. + apply const_pathS_LT with n; auto. + unfold m; abstract lia. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)