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