proposition: Lemma trunc_app : forall (v1 v2 : list A) (i : nat), trunc (v1 ++ v2) i = trunc v1 i ++ trunc v2 (i - length v1).
proof: Proof. simple induction v1. simpl in |- *. auto with arith. intros. rewrite app_eq2. rewrite length_eq2. elim i. simpl in |- *. rewrite trunc_O. trivial with arith. intros. simpl in |- *. rewrite H. trivial with arith. Qed.
imports: Arith_compl Minus Lists_compl