proposition: Remark R13 : (0 < l)%nat -> gamma <> zero -> standard_path (S n) alpha ((l + n)) gamma.
proof: Proof. destruct l. - intro H; destruct (Nat.lt_irrefl _ H). - intros H Hg; replace ((S n0) + n)%nat with ( n0 + S n)%nat. + unfold gamma; apply standard_gnaw_to_path. * apply Rem02. * discriminate. * unfold gamma in Hg; intro H0; apply standard_gnaw_S_zero in H0; contradiction. + abstract lia. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)