Rework lemmas for `take/drop` of an `++`:

• Add take_app and drop_app, which are the strongest versions, and use take_app_X for derived versions.
• Consistently use ' suffix for version with premise n = length, and have versions without ' with length inlined.
• Rename take_app → take_app_length, take_app_alt → take_app_length', take_add_app → take_app_add', take_app3_alt → take_app3_length', drop_app → drop_app_length, drop_app_alt → drop_app_length', drop_add_app → drop_app_add', drop_app3_alt → drop_app3_length'.

This closes #197 (closed).

stdpp/countable.v

@@ -355,7 +355,7 @@ Proof.
   - rewrite <-(assoc_L _). revert k. generalize ([inl (length ts, n)] ++ l).
     induction ts as [|t ts'' IH]; intros k ts'''; csimpl; auto.
     rewrite reverse_cons, <-!(assoc_L _), FIX; simpl; auto.
-  - simpl. by rewrite take_app_alt, drop_app_alt, reverse_involutive
+  - simpl. by rewrite take_app_length', drop_app_length', reverse_involutive
       by (by rewrite reverse_length).
 Qed.