proposition: Theorem rev_length : forall l : natlist, length (rev l) = length l.
proof: Proof. intros l. induction l as [| n l' IHl']. - reflexivity. - simpl. rewrite -> app_length. simpl. rewrite -> IHl'. rewrite add_comm. reflexivity. Qed.