proposition: Theorem rev_length : forall (lst : natlist), length (rev lst) = length lst.
proof: Proof. intros lst. induction lst as [| h t]. - reflexivity. - simpl. rewrite -> app_length. simpl. rewrite -> IHt. rewrite add_comm. reflexivity. Qed.