proposition: Remark R15 : gamma <> zero -> (0 < l)%nat -> const_path (n + l) alpha gamma.
proof: Proof. intros Hg H; specialize (@flatten (S n) alpha (n + l) (standard_gnaw (S n) alpha l)); intro H0; apply H0; auto with arith. - generalize (R13 H);intro; simpl in H1; replace (n+l)%nat with (l+n)%nat; auto with arith. - apply not_zero_lt; auto. apply Rem02. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)