proposition: Lemma ler_weXz2l x (x1 : 1 <= x) : {homo exprz x : x y / x <= y}.
proof: Proof. move=> m n /= hmn; case: (lerP 0 m)=> [|/ltW] hm. by rewrite ler_wpeXz2l // [_ \in _](le_trans hm). case: (lerP n 0)=> [|/ltW] hn. by rewrite ler_wneXz2l // [_ \in _](le_trans hmn). apply: (@le_trans _ _ (x ^ 0)); first by rewrite ler_wneXz2l. by rewrite ler_wpeXz2l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)