proposition: Lemma standard_gnaw_to_path : forall t alpha i, alpha <> zero -> i <> 0 -> standard_gnaw i alpha t <> zero -> standard_path i alpha (t + i)%nat (standard_gnaw i alpha (S t)).
proof: Proof. induction t. - simpl. intros. left; auto. - intros ; right. specialize (IHt (canon alpha i) (S i)); destruct (T1_eq_dec (canon alpha i) zero). + simpl in H1; rewrite e in H1; rewrite standard_gnaw_zero in H1; now destruct H1. + specialize (IHt n); cbn ; replace (t + S i)%nat with (S (t+i))%nat in IHt. * apply IHt; auto. * cbn in H1; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)