proposition: Lemma ratR_pinv a : (0 < a)%R -> a^-1%R == a^-1.
proof: Proof. move=> a_gt0; have aR_gt0: 0 < a by rewrite -ratR0; apply/ratR_ltP. apply: (pmulIR aR_gt0); rewrite -ratRM mulRC (divRR (gtR_neq aR_gt0)). by rewrite mulVf ?ratR1 ?gt_eqF. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)