fact: Fixpoint sqrt_aux (p:positive) : {s:Z &{r:Z | Zpos p = s*s+r /\ 0 <= r <= 2*s}} := match p return {s:Z & (sqrt_type1 p s)} with 1%positive => existT (sqrt_type1 1) 1 (exist (sqrt_type2 1 1) 0 th_sqrt1) | 2%positive => existT (sqrt_type1 2) 1 (exist (sqrt_type2 2 1) 1 th_sqrt2) | 3%positive => existT (sqrt_type1 3) 1 (exist (sqrt_type2 3 1) 2 th_sqrt3) | xO (xO p') => match sqrt_aux p' with (existT _ s' (exist _ r' h)) => match Z_le_gt_dec (4*s'+1) (4*r') with left h' => (existT (sqrt_type1 (xO (xO p'))) (2*s'+1) (exist (sqrt_type2 (xO (xO p')) (2*s'+1)) ((4*r')-(4*s'+1)) (th_sqrt_4_0_le p' s' r' h h'))) | right h' => (existT (sqrt_type1 (xO (xO p'))) (2*s') (exist (sqrt_type2 (xO (xO p')) (2*s')) (4*r') (th_sqrt_4_0_gt p' s' r' h h'))) end end | xO (xI p') => match sqrt_aux p' with (existT _ s' (exist _ r' h)) => match Z_le_gt_dec (4*s'+1) (4*r'+2) with left h' => (existT (sqrt_type1 (xO (xI p'))) (2*s'+1) (exist (sqrt_type2 (xO (xI p')) (2*s'+1)) ((4*r'+2)-(4*s'+1)) (th_sqrt_4_2_le p' s' r' h h'))) | right h' => (existT (sqrt_type1 (xO (xI p'))) (2*s') (exist (sqrt_type2 (xO (xI p')) (2*s')) (4*r'+2) (th_sqrt_4_2_gt p' s' r' h h'))) end end | xI (xO p') => match sqrt_aux p' with (existT _ s' (exist _ r' h)) => match Z_le_gt_dec (4*s'+1) (4*r'+1) with left h' => (existT (sqrt_type1 (xI (xO p'))) (2*s'+1) (exist (sqrt_type2 (xI (xO p')) (2*s'+1)) ((4*r'+1)-(4*s'+1)) (th_sqrt_4_1_le p' s' r' h h'))) | right h' => (existT (sqrt_type1 (xI (xO p'))) (2*s') (exist (sqrt_type2 (xI (xO p')) (2*s')) (4*r'+1) (th_sqrt_4_1_gt p' s' r' h h'))) end end | xI (xI p') => match sqrt_aux p' with (existT _ s' (exist _ r' h)) => match Z_le_gt_dec (4*s'+1) (4*r'+3) with left h' => existT (sqrt_type1 (xI (xI p'))) (2*s'+1) (exist (sqrt_type2 (xI (xI p')) (2*s'+1)) ((4*r'+3)-(4*s'+1)) (th_sqrt_4_3_le p' s' r' h h')) | right h' => existT (sqrt_type1 (xI (xI p'))) (2*s') (exist (sqrt_type2 (xI (xI p')) (2*s')) (4*r'+3) (th_sqrt_4_3_gt p' s' r' h h')) end end end.
imports: ZArith ZArithRing Extraction Lia