proposition: Lemma le_length_trunc : forall (v : list A) (i : nat), length (trunc v i) <= i.
proof: Proof. simple induction v. simpl in |- *. auto with arith. intros. case i. rewrite trunc_O. auto with arith. intro. simpl in |- *. apply le_n_S. apply H. Qed.
imports: Arith_compl Minus Lists_compl