proposition: Lemma invRK x : x^-1^-1 == x.
proof: Proof. have [-> | nz_x] := reals_classic (x == 0); first by rewrite !invR0. by have nz_vx := invR_neq0 nz_x; apply/(mulIR nz_vx); rewrite mulRC !divRR. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)