proposition: Theorem th_sqrt_4_0_le : forall p s r, Zpos p = s*s+r /\ 0<= r <= 2*s -> 4*s+1 <= 4*r -> Zpos(xO (xO p)) = (2*s+1)*(2*s+1)+(4*r - (4*s+1)) /\ 0<= 4*r-(4*s+1) <= 2*(2*s+1).
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