fact: Definition sqrtrem_step (f g:positive->positive) p := match p with | (s, IsPos r) => let s' := s~0~1 in let r' := g (f r) in if s' <=? r' then (s~1, sub_mask r' s') else (s~0, IsPos r') | (s,_) => (s~0, sub_mask (g (f 1)) 1~0~0) end.
imports: BinNums