proposition: Lemma flatten : forall (i:nat) alpha (j:nat) beta, standard_path i alpha j beta -> nf alpha -> zero t1< alpha -> (0 < i)%nat -> const_path j alpha beta.
proof: Proof. induction 1. - subst; simpl; intros; destruct i. + now destruct H2. + now left. - intros; assert (0 < j)%nat. { generalize (standard_path_to_le_inv H). intro; auto with arith. lia. } + destruct (T1_eq_dec (canon alpha i) zero) as [e | ne]. { rewrite e in H; assert (beta = zero). { generalize (standard_path_zero H); auto. } subst beta; destruct i. - inversion H2. - destruct (canonS_zero_inv _ _ e). + subst; red; destruct j. * inversion H3. * left; apply standard_path_origin in H; now destruct H. + destruct j. * inversion H3. * left; split. -- intro; subst; discriminate H5. -- subst; reflexivity. } destruct j. * inversion H3. * destruct i. -- inversion H2. -- apply const_pathS_trans with (canon alpha (S i)). ++ apply Cor12_1 with i; auto. ** apply canonS_LT;auto. intro; subst; auto with T1. ** apply standard_path_to_le_inv in H; abstract lia. ** left; split. intro; subst; auto with T1. reflexivity. ++ apply IHstandard_path_to; auto. ** apply nf_canon; auto. ** apply not_zero_lt;auto. apply nf_canon; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)