Fix subuKC

The same proof works using n <=? m instead of n <? m

The new statement of the lemma is

Lemma subuKC (m n : uint) : m <=? max_int -> n <=? m -> n + (m - n) = m.