proposition: Lemma trunc_plus_petit : forall (v1 v2 : list A) (i j : nat), j <= i -> trunc v1 i = v2 -> trunc v1 j = trunc v2 j.
proof: Proof. intros. rewrite <- H0. rewrite trunc_trunc3. trivial with arith. exact H. Qed.
imports: Arith_compl Minus Lists_compl