Lean 4 proof that the Jacobian conjecture in dimension 2n implies the Poisson conjecture in dimension n, Formal Conjectures' math/0608009 statement (Adjamagbo and van den Essen, Theorem 7)