proposition: Lemma bijective_contract : {on [pred r | `|r| <= 1]%R, bijective (@contract R)}.
proof: Proof. exists (@expand R); [exact: in1W contractK | exact: (@expandK R)]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal