proposition: Lemma lee_sqrt x y : 0 <= y -> (sqrte x <= sqrte y) = (x <= y).
proof: Proof. case: x y => [x||] [y||] yge0 //=. - exact: mathcomp_extra.ler_sqrt. - by rewrite !leey. - by rewrite leNye lee_fin sqrtr_ge0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed