proposition: Remark R18 : gamma <> zero -> (0 < l)%nat -> const_pathS (n+l) alpha gamma.
proof: Proof. intros Hg H; generalize (R15 Hg H); case_eq (n + l)%nat. - intro; assert False by abstract lia; contradiction. - intros n0 H1 H2; apply Cor12_1 with n0;auto. apply const_pathS_LT with n0;auto; apply Rem02. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)