Functions defined by cases without match

Consider the following type definition for vehicles (including bicycles and motorized vehicles). For bicycles, we can have a variable number of seats and for motorized vehicles we can have a variable number of seats and a variable number of wheels:
Inductive vehicle : Set :=
  | bicycle : nat -> vehicle 
  | motorized : nat -> nat -> vehicle.
Define a function computing the number of seats of any vehicle, as an application of vehicle_rec (without using match ... with ).

Solution

This file