proposition: Lemma sup_contract_le1 S : S !=set0 -> (`|sup (contract @` S)| <= 1)%R.
proof: Proof. case=> x Sx; rewrite ler_norml; apply/andP; split; last first. apply sup_le_ub; first by exists (contract x), x. by move=> r [y Sy] <-; case/ler_normlP : (contract_le1 y). rewrite (@le_trans _ _ (contract x)) //. by case/ler_normlP : (contract_le1 x); rewrite lerNl. apply sup_ub; last by exists x. by exists 1%R => r [y Sy <-]; case/ler_normlP : (contract_le1 y). 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