chore(order/lexicographic): cleanup (#11299)
Changes include:
* factoring out `prod.lex.trans` from the proof of `le_trans` in `prod.lex.has_le`, and similarly for `antisymm` and `is_total`
* adding some missing `to_lex` annotations in the `prod.lex.{le,lt}_def` lemmas
* avoiding reproving decidability of `prod.lex`
* replacing some proofs with pattern matching to avoid getting type-incorrect goals where `prod.lex.has_le` appears comparing terms that are not of type `lex`.
