proposition: Remark R17 : (0 < l)%nat -> const_pathS (n+l) alpha beta.
proof: Proof. intro H; generalize (R16 H); intro H0. case_eq (n + l)%nat. - intro H1; assert False by abstract lia; contradiction. - intros n0 H1; rewrite H1 in *; apply Cor12_1 with n0;auto. apply Rem0. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)