proposition: Lemma ler_psqrt : {in @nneg R &, {mono sqrt : a b / a <= b}}.
proof: Proof. apply: le_mono_in => x y x_gt0 y_gt0. rewrite !lt_neqAle => /andP[neq_xy le_xy]. by rewrite ler_wsqrtr // eqr_sqrt // neq_xy. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)