proposition: Lemma expandK : {in [pred r | `|r| <= 1]%R, cancel expand contract}.
proof: Proof. move=> r; rewrite inE le_eqVlt => /orP[|r1]. rewrite eqr_norml => /andP[/orP[]/eqP->{r}] _; by [rewrite expand1|rewrite expandN1]. rewrite /expand 2!leNgt ltrNl; case/ltr_normlP : (r1) => -> -> /=. have r_pneq0 : (1 + r / (1 - r) != 0)%R. rewrite -[X in (X + _)%R](@divrr _ (1 - r)%R) -?mulrDl; last first. by rewrite unitfE subr_eq0 eq_sym lt_eqF // ltr_normlW. by rewrite subrK mulf_neq0 // invr_eq0 subr_eq0 eq_sym lt_eqF // ltr_normlW. have r_nneq0 : (1 - r / (1 + r) != 0)%R. rewrite -[X in (X + _)%R](@divrr _ (1 + r)%R) -?mulrBl; last first. by rewrite unitfE addrC addr_eq0 gt_eqF // ltrNnormlW. rewrite addrK mulf_neq0 // invr_eq0 addr_eq0 -eqr_oppLR eq_sym gt_eqF //. exact: ltrNnormlW. wlog : r r1 r_pneq0 r_nneq0 / (0 <= r)%R => wlog_r0. have [r0|r0] := lerP 0 r; first by rewrite wlog_r0. move: (wlog_r0 (- r)%R). rewrite !(normrN, opprK, mulNr) oppr_ge0 => /(_ r1 r_nneq0 r_pneq0 (ltW r0)). by move/eqP; rewrite eqr_opp => /eqP. rewrite /contract !ger0_norm //; last first. by rewrite divr_ge0 // subr_ge0 (le_trans _ (ltW r1)) // ler_norm. apply: (@mulIr _ (1 + r / (1 - r))%R); first by rewrite unitfE. rewrite -(mulrA (r / _)) mulVr ?unitfE // mulr1. rewrite -[X in (X + _ / _)%R](@divrr _ (1 - r)%R) -?mulrDl ?subrK ?div1r //. by rewrite unitfE subr_eq0 eq_sym lt_eqF // ltr_normlW. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed