Update AugmentedSimplexCategory.v

This file adopts a mix of Qed and Defined proof terminations depending on whether the thing being proved is a proposition or something with computational content that needs to be unfolded. When it is difficult to separate the two, the tactic 'abstract' is used to opaque subproofs i.e. of is_nat_trans.

Unused and commented out lemmas have been deleted.

The table of contents has been updated and reorganized, square brackets [ - ] have been added to the names of identifiers for coqdoc.

The file has been expanded with proofs that FinCard and FinOrd are *strict* monoidal categories.