proposition: Lemma lee_sqrE x y : 0 <= y -> x ^+ 2 <= y ^+ 2 -> x <= y.
proof: Proof. move=> yge0; have [xge0|xlt0 x2ley2] := leP 0 x; first by rewrite lee_sqr. exact: le_trans (ltW xlt0) _. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed