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