fact: Fixpoint root_loop (x : Dyadic Z) (n : nat) : Dyadic Z * Dyadic Z := match n with | O => (x, 0) | S n => let (r, s) := root_loop x n in if decide_rel (≤) (s + 1) r then ((r - (s + 1)) ≪ 2, (s + 2) ≪ 1) else (r ≪ 2, s ≪ 1) end.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.implementations.dyadics MathClasses.implementations.fast_integers