proposition: Theorem Kroot_spec r : if Kroot r is Some r1 then r1 ^+ 2 = r else forall k, k ^+2 != r.
proof: Proof. by rewrite /Kroot; case: pickP => [x /eqP//| P k]; rewrite (P k). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra ring)