proposition: Lemma trunc_max : forall (v : list A) (i : nat), length v <= i -> trunc v i = v.
proof: Proof. simple induction v. simpl in |- *. trivial with arith. intros. inversion H0. rewrite trunc_all. trivial with arith. simpl in |- *. rewrite H. trivial with arith. apply le_Sn_le. generalize H1. simpl in |- *. trivial with arith. Qed.
imports: Arith_compl Minus Lists_compl