proposition: Lemma level_ge: forall (s t : stack A), (truncate (length t) s, t) = level s t <-> length t <= length s.
proof: Proof. split;intros. unfold level in H. case_eq (Nat.compare (length t) (length s));intros. apply nat_compare_Eq in H0. rewrite H0. trivial. apply nat_compare_lt in H0. auto with *. assert (truncate (length t) s = s). unfold truncate. destruct s. simpl. destruct (Nat.compare (length t) 0);trivial. rewrite H0. trivial. rewrite H1 in H. apply nat_compare_lt_gt_sym in H0. rewrite H0 in H. inversion H. generalize truncate_1. intro. specialize H2 with (length s) t. apply nat_compare_lt_gt_sym in H0. apply nat_compare_gt in H0. assert ((length s) <= (length t)). auto with *. apply H2 in H4. rewrite <- H4. trivial. unfold level. case_eq(Nat.compare (length s) (length t));intros. unfold truncate. destruct s. simpl. destruct (Nat.compare (length t) 0);trivial. apply nat_compare_eq_sym in H0. rewrite H0;trivial. apply nat_compare_ge in H. elim H;trivial. trivial. Qed.
imports: Coq(List) Coq(Arith)