proposition: Lemma length_rev : forall l : list A, length (rev l) = length l.
proof: Proof. simple induction l; auto with arith. intros. simpl in |- *. rewrite length_app. simpl in |- *. rewrite plus_n_SO. rewrite H. trivial with arith. Qed.
imports: List Arith_compl