proposition: Lemma sqr_sqrte x : 0 <= x -> sqrte x ^+ 2 = x.
proof: Proof. case: x => [x||] xge0; rewrite expe2 ?mulyy//. by rewrite -sqrteM// -EFinM/= sqrtr_sqr ger0_norm. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed