proposition: Lemma length_trunc : forall (v : list A) (i : nat), i <= length v -> length (trunc v i) = i.
proof: Proof. simple induction v. simpl in |- *. auto with arith. intros b b0 H. simple induction i. simpl in |- *. trivial with arith. simpl in |- *. intros. apply eq_S. apply H. apply le_S_n. exact H1. Qed.
imports: Arith_compl Minus Lists_compl