fact: Fixpoint sqrtrem p : positive * mask := match p with | 1 => (1,IsNul) | 1~0 => (1,IsPos 1) | 1~1 => (1,IsPos 1~0) | p~0~0 => sqrtrem_step xO xO (sqrtrem p) | p~0~1 => sqrtrem_step xO xI (sqrtrem p) | p~1~0 => sqrtrem_step xI xO (sqrtrem p) | p~1~1 => sqrtrem_step xI xI (sqrtrem p) end.
imports: BinNums