proposition: Remark R20 : gamma <> zero -> (0 < l)%nat -> beta t1< gamma -> const_pathS (n+l) gamma beta.
proof: Proof. intros; apply Proposition_2_3a with alpha; auto. - apply Rem02. - apply R17; auto. - apply R18;auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)