proposition: Lemma invRM x y : (x * y)^-1 == x^-1 / y.
proof: Proof. have [-> | nzx] := reals_classic (x == 0); first by rewrite !(invR0, mul0R). have [-> | nzy] := reals_classic (y == 0); first by rewrite !(invR0, mulR0). have nzxy: x * y != 0 by rewrite -(mulR0 x) => /(mulRI nzx). by apply/(mulRI nzxy); rewrite mulRACA !divRR ?mulR1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)