proposition: Lemma standard_gnaw_S_zero : forall i n alpha , standard_gnaw n alpha i = zero -> standard_gnaw n alpha (S i)=zero.
proof: Proof. induction i. - simpl; intros; subst; apply canon_zero. - intros; replace (S (S i)) with (S i + 1)%nat; [| lia]. rewrite standard_gnaw_plus, H, standard_gnaw_zero; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)