Significant automation improvements. Partnering has been implemented,…

… which can associate two terms next to each other (even within a tensor, though it will not manipulate tensors to make this happen). It also has support for generic Ltac tests on the two terms, which allowed the creation of tactics to automatically cancel isomorphisms with their inverses (regardless of association). Furthermore, this has been extended to partnering on a sequence of terms, which reassociates to make a prescribed series of terms be left-associated within a larger expression (again, compatibly with tensors, though not manipulating them). By making this sequence of terms be evars, the tactic partners_rw was implemented, which takes a lemma whose form (up to any number of quantifiers before it) is the equivalence of morphisms, finds a reassociation of a term in the goal such that that lemma can be rewritten, and performs that rewrite. This tactic has not been extensively tested, and is — likely somewhat unavoidably — not excessively performant (on the scale of one or a few tenths of a second for a rewrite on a moderately-sized goal).