proposition: Lemma app_v_nil_sym : forall v1 v2 : list A, v1 = nil -> v1 ++ v2 = v2 ++ v1.
proof: Proof. simple induction v2. intro. rewrite H. trivial with arith. intros. rewrite H0. auto with arith. Qed.
imports: List Arith_compl