proposition: Lemma mulV x : x != 0 -> x * x^-1 == 1.
proof: Proof. elim/opp_ind: x => [x IHx | x le0x] nz_x. by rewrite -(oppK x^-1) -invN mulRN -mulNR IHx // -opp0 => /eqR_opp2. rewrite /inv; set y := `|x|^-1; case: ifR_cases => // _ ->. have{nz_x} [a lt0a leax]: exists2 a, 0 < a & x >= a. by have [[a] | /(gec0N_eq0 le0x)//] := ltcP (- x) 0; rewrite oppr0; exists a. pose E z := `|x|*|z| < 1; have E_0: E 0 by rewrite /E amulC amul0. have supE: has_sup E. split; [by exists 0 | exists a^-1%R => //]. move=> z [b ltxb [lt_z_vb _]]; apply/ltcW/(ltc_trans lt_z_vb). by rewrite mul1r (ltf_pinv (abs_ge0 ltxb)) ?(gec_lt_trans _ ltxb) // => -[]. have ubEy: ub E y by apply: sup_ub. have le0y: y >= 0 by apply/leRq/ubEy. rewrite ge0_mul //; split=> [b lt1b | b [c ltxc [ltybc _]]]; last first. have [d ltxd ltdc] := open ltxc. have [c_gt0 d_gt0] := (abs_ge0 ltxc, abs_ge0 ltxd). suffices: (1 / c < b / c)%R by rewrite ltr_pmul2r ?invr_gt0. apply: gec_lt_trans ltybc; apply/leRq/ubEy; exists d => //. by rewrite !mul1r ge0_abs ltcE ?ltf_pinv // lt_gtF ?invr_gt0. have lt0b: 0 < b by apply: lt_trans lt1b. pose e := (1 - b^-1)%R; have lt0e: 0 < e by rewrite ltcE subr_gt0 invf_lt1. have [c ltxc [d lt_cea_d ledx]]: x - x < a * e by rewrite addN ltcE mulr_gt0. have ltac: a < c := gec_lt_trans leax ltxc. have lt0c: 0 < c := lt_trans lt0a ltac. have lt0d: 0 < d. apply: lt_trans lt_cea_d; rewrite opprB subr_gt0 mulrBr mulr1. by rewrite ltr_snsaddr // oppr_lt0 divr_gt0. have le_y_vd: y <= d^-1%R. apply/sup_le_ub=> // z -[f ltxf [lt_z_vf _]]; apply/ltcW/(ltc_trans lt_z_vf). by rewrite mul1r (ltf_pinv (abs_ge0 ltxf)) ?(gec_lt_trans _ ltxf) // => -[]. exists c; rewrite ge0_abs //; apply: le_y_vd; rewrite ltcE. rewrite -invf_div ltf_pinv ?rpred_div //; apply: lt_trans lt_cea_d. by rewrite ltr_oppr -[c in (_ - c)%R]mulr1 ltr_subl_addl -mulrBr ltr_pmul2r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)