fact: Definition sqrt_nat' : forall n, ({s : nat & {r : nat | n = s * s + r /\ n < (s + 1) * (s + 1)}}) := well_founded_induction lt_wf (fun n => {s : nat & {r : nat | n = s * s + r /\ n < (s + 1) * (s + 1)}}) sqrt_nat_F.
imports: Arith ArithRing Lia Compare_dec Wf_nat