fact: Definition iter2_sqrt := Eval lazy beta delta [sqrt2_step] in fix iter2_sqrt (n: nat) (rec: int -> int -> int -> int) (ih il j: int) {struct n} : int := sqrt2_step (fun ih il j => match n with | O => rec ih il j | S n => (iter2_sqrt n (iter2_sqrt n rec)) ih il j end) ih il j.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63