proposition: Lemma path_toS_mult alpha s i : nf alpha -> path_toS zero s (T1.phi0 alpha) -> path_toS (T1.cons alpha i zero) s (T1.cons alpha (S i) zero).
proof: Proof. inversion 2. - subst; inversion H1. assert (alpha = zero). { destruct H1; symmetry in H3. apply canonS_zero_inv in H3; destruct H3. - discriminate. - now injection H3. } subst; left; split. + discriminate. + now simpl. - subst; right with (T1.cons alpha i gamma). + split. * discriminate. * rewrite canon_SSn_zero. f_equal. -- destruct H1; auto. -- auto. + apply path_toS_tail; auto. apply nf_intro; [auto | | ]. * destruct H1; subst. apply nf_canon; now apply nf_phi0. * apply lt_a_phi0_b_phi0R. destruct H1; subst. generalize (@canonS_LT i0 (T1.phi0 alpha) (nf_phi0 H)). destruct 1. -- discriminate. -- tauto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)