proposition: Lemma mlarge_iff alpha x (s:list nat) : s <> nil -> ~ In 0 (x::s) -> mlarge alpha (x::s) <-> gnaw alpha (but_last x s) = one.
proof: Proof. intros H H0; split. - intros H1; rewrite mlarge_unshift in H1; auto. rewrite gnaw_gnawS, unshift_but_last; auto. + simpl in H1; destruct x. * destruct H0; left; auto. * simpl; simpl in H1; rewrite mlargeS_iff in H1; auto. apply unshift_not_nil; auto. -- intro; apply H0; now right. - rewrite mlarge_unshift; auto. rewrite gnaw_gnawS; destruct x. + destruct H0; now left. + simpl; rewrite unshift_but_last; auto. simpl; rewrite mlargeS_iff; auto. apply unshift_not_nil; intro; apply H0; now right. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)