proposition: Theorem make_list_end : forall (A:Type) (a:A) (n:nat) (l:list A), make_list A a (S n) ++ l = make_list A a n ++ a :: l.
proof: Proof. simple induction n; simpl. - trivial. - intros n' H l; rewrite H; trivial. Qed.
imports: List Arith