HOL is a total logic, so all functions must be defined for all inputs of
the corresponding type. In Isabelle/HOL, division by zero is therefore
defined to yield zero, and with that, the lemma you cited holds.
Understanding the definitions of the constants involved in a statement
and how they differ from ‘standard’ mathematical definitions is crucial.
Post by Omar Jasim
"[|a ≤ b; 0 ≤ c|] ==> a/c ≤ b/c"
by (force simp add: divide_strict_right_mono le_less)
here 0 ≤ c which I think it should be 0 < c as the division cann't done for