solve the alternate problem (3 stars). i thought of 3 ways that worked; the last works with the least fuss. Coq's fixpoint decreasing restriction is pretty restrictive. interesting to compare the first and last