§2.5: explain how to call inf_le_left when arguments are not inferrable#323

darijgr wants to merge 2 commits intoavigad:masteravigad/mathematics_in_lean_source:masterfrom

darijgr:patch-1darijgr/mathematics_in_lean_source:patch-1Copy head branch name to clipboard