proposition: Theorem rev_length_firsttry : forall (lst : natlist), length (rev lst) = length lst.
proof: Proof. intros lst. induction lst as [| h t]. - reflexivity. - simpl. rewrite <- IHt. Abort. Theorem app_length : forall (lst1 lst2 : natlist), length (lst1 ++ lst2) = (length lst1) + (length lst2). Proof. intros lst1 lst2. induction lst1 as [| h1 t1]. - reflexivity. - simpl. rewrite IHt1. reflexivity. Qed.