feat: define right congruence and prove its basic properties

[ctchou]

This PR defines the notion of a "right congruence", which is an equivalence relation between finite words that is preserved by concatenation on the right, and proves its basic properties:

• There is a natural deterministic automaton corresponding to each right congruence whose states are the equivalence classes of the congruence and whose transitions correspond to concatenation on the right of the input symbols.
• If a right congruence is of finite index, then each of its equivalence classes is a regular language.

We will eventually prove the closure of omega-regular languages under complementation by constructing a right congruence of finite index with certain special properties.

Right congruences are also intimately related to the Myhill-Nerode theorem, but currently we do not plan to pursue that direction.

[ctchou]

Rebase on upstream/main.

[chenson2018]

This all looks reasonable to me, but would you mind posting in the "Is There Code for X?" channel to see if anyone has thoughts about RightCongruence/RightCongruence.QuotType/RightCongruence.eqvCls?

[ctchou]

Per your suggestion, I have posted a query on Zulip: https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Right.20congruence/with/568624176

[ctchou]

I'm not sure the CovariantClass that Eric Wieser pointed out in the Zulip thread is appropriate here. The comments at the beginning of Mathlib.Algebra.Order.Monoid.Unbundled.Defs indicate that the underlying binary relation is intended to be an order, but in our application that relation is an equivalence relation.