proposition: Theorem th_sqrt_4_3_gt : 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)*(2*s)+(4*r+3) /\ 0<= 4*r+3 <= 2*(2*s).
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