# Module sub_square

``` Require Export sqrt_prog. Require Export sub_goals. Require Export sub_goals2. Correctness square_s_and_sub   fun (np : nat)(sp : nat)(nn:nat) (l: nat ref)(h:nat ref)       (q : Z ref)(c:Z ref) (b:Z ref) ->   {(lt (S O) nn) /\ (l=(div2' nn))/\(h=(minus nn (div2' nn))) /\       `np + 2*nn<=bound`/\ `sp +nn <= bound`/\       (`np+2*nn <= sp`\/`sp + nn <= np`) /\       `q*(pow beta l) + (I m sp l) <= (pow beta l)` /\ `0 <= q <= 1`} begin   (mpn_sqr_n (plus np nn) sp !l);   (mpn_sub_n np np (plus np nn) (mult (S (S O)) !l));   b := !q + (bool2Z !rb);   if (nat_eq_bool !l !h) then      c := !c - !b   else      begin        (mpn_sub_1 (plus np (mult (S (S O)) !l))                   (plus np (mult (S (S O)) !l))                   (S O) !b);        c := !c - (bool2Z !rb)      end end {`(I m np nn)=(c@-c) * (pow beta nn) +                        (I m@ np nn) - (q@ * (pow beta l) + (I m@ sp l))*                                          (q@ * (pow beta l) + (I m@ sp l))` /\         (p:nat)`0<=p<bound`->~((le np p)/\(lt p (plus np (mult (S (S O)) nn)))) ->                   (access m p)=(access m@ p)}. Apply sub_goal1 with   np := np sp := sp nn := nn h:= h l := l m := m q:=q;Assumption. Apply sub_goal2 with   np := np sp := sp nn := nn h:= h l := l m := m q:=q   m0 := m0;Assumption. Apply sub_goal3 with   np := np sp := sp nn := nn h:= h l := l m := m q:=q   m0 := m0 rb0 := rb0 m1 := m1;Assumption. Apply sub_goal4 with   np := np sp := sp nn := nn h:= h l := l m := m q:=q   m0 := m0 rb0 := rb0 m1 := m1;Assumption. Apply sub_goal5 with   np := np sp := sp nn := nn h:= h l := l m := m q:=q   m0 := m0 rb0 := rb0 m1 := m1 rb1 := rb1 m2 := m2;Assumption. Defined. ```

``` ```

Index
This page has been generated by coqdoc