proposition: Theorem th_sqrt_4_0_gt : forall p s r, Zpos p = s*s+r /\ 0<= r <= 2*s -> 4*s+1 > 4*r -> Zpos(xO (xO p)) = (2*s)*(2*s)+4*r /\ 0<= 4*r <= 2*(2*s).
proof: Proof. intros p s r [Heq Hlt] Hle; rewrite Zpos_xO; rewrite (Zpos_xO p). rewrite Heq; split. - ring. - split; lia. Qed.
imports: ZArith ZArithRing Extraction Lia