proposition: Lemma le_expand_in : {in [pred r | `|r| <= 1]%R &, {mono expand : x y / (x <= y)%O}}.
proof: Proof. exact: can_mono_in (onW_can_in predT expandK) _ (in2W le_contract). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed