proposition: Lemma mlarge_unicity alpha k l l' : mlarge alpha (interval (S k) l) -> mlarge alpha (interval (S k) l') -> l = l'.
proof: Proof. intros H H0; assert (H1 : (S k<= l)%nat) by (eapply path_to_interval_inv_le; eauto). assert (H2 : (S k <= l')%nat) by (eapply path_to_interval_inv_le; eauto). destruct (Compare_dec.lt_eq_lt_dec l l') as [[Hlt | Heq] | Hgt]; auto. - rewrite (interval_app (S k) l l') in H0; [|try lia| try lia]. destruct (@path_to_appR _ _ _ H0 (interval (S k) l) (interval (S l) l')); trivial. + apply interval_not_empty; auto. + apply interval_not_empty; auto. + intro H3; destruct (in_app_or _ _ _ H3). * apply (@interval_lt_not_In 0 (S k) l); auto with arith. * apply (@interval_lt_not_In 0 (S l) l'); auto with arith. + destruct H3 as [H3 H4]. assert (x = zero). { apply path_to_gnaw in H; apply path_to_gnaw in H3; congruence. } subst; destruct (path_to_zero H4). - rewrite (interval_app (S k) l' l) in H; [| try lia | try lia]. destruct (@path_to_appR _ _ _ H (interval (S k) l') (interval (S l') l)); trivial. apply interval_not_empty; auto. apply interval_not_empty; auto. + intro H3; destruct (in_app_or _ _ _ H3). apply (@interval_lt_not_In 0 (S k) l'); auto with arith. apply (@interval_lt_not_In 0 (S l') l); auto with arith. + destruct H3. assert (x = zero). { apply path_to_gnaw in H0; apply path_to_gnaw in H3; congruence. } subst; destruct (path_to_zero H4). Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)