proposition: Lemma le_expand : {homo expand : x y / (x <= y)%O}.
proof: Proof. move=> x y xy; have [x1|] := lerP `|x| 1. have [y_le1|/ltW /expand1->] := leP y 1%R; last by rewrite leey. rewrite le_expand_in ?inE// ler_norml y_le1 (le_trans _ xy)//. by rewrite lerNl (ler_normlP _ _ _). rewrite ltr_normr => /orP[|] x1; last first. by rewrite expandN1 // ?leNye // lerNr ltW. by rewrite expand1; [rewrite expand1 // (le_trans _ xy) // ltW | exact: ltW]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed