proposition: Lemma truncate_truncate: forall n m (s : stack A), n <= m -> truncate n s = truncate n (truncate m s).
proof: Proof. induction s. intuition. repeat rewrite truncate_n_nil;trivial. intros. generalize H. intros. apply IHs in H0. unfold truncate. case_eq (Nat.compare m (length (a::s))). case_eq (Nat.compare n (length (a::s))). trivial. trivial. trivial. unfold truncate in H0. rewrite <- H0. clear H0. intros. case_eq (Nat.compare n (length (a::s))). intuition. apply nat_compare_lt in H0. apply nat_compare_Eq in H1. subst. apply Nat.le_ngt in H. elim H;trivial. trivial. intuition. apply nat_compare_lt in H0. apply nat_compare_gt in H1. assert (m < n). apply lt_gt in H1. apply Nat.lt_trans with (length (a::s));trivial. apply Nat.le_ngt in H. elim H;trivial. trivial. Qed.
imports: Coq(List) Coq(Arith)