proposition: Lemma truncate_1: forall n (s : stack A), n <= length s -> n = length ( truncate n s).
proof: Proof. intros. unfold truncate in |- *. induction s. simpl in *. assert (n = 0) by auto with arith. destruct Nat.compare; trivial. case_eq (Nat.compare n (length (a :: s))); intro. apply nat_compare_Eq in H0; trivial. apply IHs. clear IHs. apply nat_compare_lt in H0. unfold length in H0. auto with *. apply nat_compare_gt in H0. apply Nat.le_ngt in H. elim H. trivial. Qed.
imports: Coq(List) Coq(Arith)