proposition: Lemma invN x : (- x)^-1 == - x^-1.
proof: Proof. rewrite /inv /`|_|^-1; setoid_rewrite amulN; rewrite -/`|x|^-1. have [/gec0_opp-le0nx -> | le0x ->] := ifR_cases (x < 0). by rewrite oppK; case: ifR_cases. by case: ifR_cases => // /(gec0N_eq0 le0x)-> ->; rewrite ainv0 opp0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)