4658ee6927738e3b54f54e64fed146124558797b161bc3ec280f8b64280ef020 evidence/A317940_upstream_cd729cdd.lean dbe610e3c24d376b9efa1b2228fed7b0bb1a16a9a4218a7ec10392e7adfd1402 proofs/lean/A317940/A317940.lean e00166189860fb26678cca207d3453bf48c540a0f2c215a5dc9ac61e17510ab8 math/a317940/proof/A317940_verified.lean