Comment by eisbaw

the tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean.