tactics for Ord and compare

Stream: Is there code for X?

[Michael George]

I’m working with a LinearOrderedCommRing, And it seems simpler to state my definitions in terms of compare instead of less than. I’m finding it a little bit difficult to write simple proofs though. For example, I don’t even see how to give a simple proof of “compare 0 0 = .eq”.

Any suggestions for how to proceed?

[Alex J. Best]

The library is set up using the < and = notations/typeclasses for the most part, so I think the answer is probably that life will be more difficult than it needs to be if you use compare, and you should change your definitions. That said you probably need things like docs#compare_eq_iff_eq or docs#compare_iff to proceed if you have compare in your statements

[Kyle Miller]

You can get some more concrete suggestions with a #mwe. Very often suggestions depend strongly on all the fiddly little details.