Require Import List. Theorem app_nil : forall (A:Type) (lst : list A), lst ++ nil = lst. Proof. intros A lst. induction lst as [ | h t IH]. - trivial. - simpl. rewrite -> IH. trivial. Qed. Theorem app_assoc : forall (A:Type) (l1 l2 l3 : list A), l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3. Proof. intros A l1 l2 l3. induction l1 as [ | h t IH]. - trivial. - simpl. rewrite -> IH. trivial. Qed. (********************************************************************) Require Import Arith. Fixpoint sum_to (n:nat) : nat := match n with | 0 => 0 | S k => n + sum_to k end. Lemma sum_helper : forall n : nat, 2 * sum_to (S n) = 2 * S n + 2 * sum_to n. Proof. intros n. simpl. ring. Qed. Theorem sum_sq : forall n : nat, 2 * sum_to n = n * (n+1). Proof. intros n. induction n as [ | k IH]. - trivial. - rewrite -> sum_helper. rewrite -> IH. ring. Qed.