proposition: Lemma sqrte_fin_num x : 0 <= x -> (sqrte x \is a fin_num) = (x \is a fin_num).
proof: Proof. by case: x => [x|//|//]; rewrite !qualifE/=. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed