proposition: Lemma length_app : forall v1 v2 : list A, length (v1 ++ v2) = length v1 + length v2.
proof: Proof. simple induction v1. simpl in |- *. trivial with arith. intros. simpl in |- *. rewrite H. trivial with arith. Qed.
imports: List Arith_compl