Add theorems for various helper libraries.

Some progress

However(!): grievousness of dealing with algebra/lib is making me
rethink this.

remove lcsymtacs (github issue #666)

The lcsymtacs structure is regarded superseded as it plainly is
a shorthand for opening the following modules:
Abbrev HolKernel boolLib Tactic Tactical BasicProvers simpLib
Rewrite bossLib Thm_cont

Fixes for changes to lists (30f513317c8)

This material had LENGTH l <= n ==> DROP n l = [] as a theorem in its
helperListTheory.

The new DROP_EQ_NIL theorem is an equivalence so the AKS material
doesn't need its own theorem (which is only used twice in any case).

Rename DROP_NIL to DROP_EQ_NIL

No longer ugly collision with DROP_nil and more consistent naming with how
other thms from the same theory are named.

Also replace >= with <=.

Fix a proof broken by move of GENLIST_CONG in f5bb2b0068e

Using EVERY in (aks n) evaluation.

Ensure (aks n) is directly executable by EVAL.

AKS mechanisation (#750)

* Add to examples: AKS, with algebra and simple_complexity.