proposition: Lemma sqrtr_sqr a : sqrt (a ^+ 2) = `|a|.
proof: Proof. have /eqP : sqrt (a ^+ 2) ^+ 2 = `|a| ^+ 2. by rewrite -normrX ger0_norm ?sqr_sqrtr ?sqr_ge0. rewrite eqf_sqr => /predU1P[-> //|ha]. have := sqrtr_ge0 (a ^+ 2); rewrite (eqP ha) oppr_ge0 normr_le0 => /eqP ->. by rewrite normr0 oppr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)