LinearOrderedAddCommGroup instance for RealScalar

[lecopivo]

A type R satisfying RealScalar R does not have imply LinearOrderedAddCommGroup R.

open SciLean

variable {R} [RealScalar R]

#synth LinearOrderedAddCommGroup R -- fails

This should be fixed! Otherwise we can't use mathlibs theorems about inequalities.

[lecopivo]

Also there should be an instance for LinearOrderedCommRing R such that we can use linarith and nlinarith tactics.