proposition: Lemma ler_wsqrtr : {homo @sqrt R : a b / a <= b}.
proof: Proof. move=> a b /= le_ab; case: (boolP (0 <= a))=> [pa|]; last first. by rewrite -ltNge; move/ltW; rewrite -sqrtr_eq0; move/eqP->. rewrite -(@ler_pXn2r R 2) ?nnegrE ?sqrtr_ge0 //. by rewrite !sqr_sqrtr // (le_trans pa). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)