fact: Definition Z_4th_root_floor_plain (z: Z): Z := match z with | Zpos p => projT1 (Z_4th_root_floor p (Zle_0_pos p)) | _ => 0%Z end.
imports: List NPeano QArith Qabs Qpossec Qsums Qround Qmetric ZArith CRArith CRsum util.Qgcd Program uneven_CRplus stdlib_omissions.P stdlib_omissions.Z stdlib_omissions.Q Coq.ZArith.Zsqrt_compat