That's not necessarily an edge. https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-math...

has the example:

  0 ≤ x^2 if x : ℝ

which humans simply use without proof. The IMO doesn't challenge participants to prove everything, only the main ideas.