proposition: Lemma invRN x : (- x)^-1 == - x^-1.
proof: Proof. have [-> | nz_x] := reals_classic (x == 0); first by rewrite !(oppR0, invR0). have nz_negx: - x != 0 by rewrite -oppR0 => /oppR_inj. by apply/(mulRI nz_negx); rewrite mulRN -mulNR oppRK !divRR. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)