proposition: Lemma truncate_pop: forall n (s : stack A), length s = (S n) -> truncate n s = pop s.
proof: Proof. intros. unfold truncate in |- *. destruct s. destruct Nat.compare; trivial. rewrite H in |- *. rewrite nat_compare_n_Sn in |- *. unfold pop in |- *. assert (length s = n). unfold length in H. apply eq_add_S. trivial. destruct s. destruct Nat.compare; trivial. rewrite H0 in |- *. replace (Nat.compare n n) with Eq . trivial. symmetry. rewrite nat_compare_Eq. trivial. Qed.
imports: Coq(List) Coq(Arith)