Theorem tendsto_coe_iff

refactor(order/filter): generalize map_succ_at_top_eq to arbitrary Galois insertions; generalize tendsto_coe_iff to arbitary order-preserving embeddings

feat(data/padics): prove Hensel's lemma