proposition: Lemma bsqrt_exact_lemma_gt : forall n q r s' r':nat, n = 4 * q + r -> q = s' * s' + r' -> 4 * s' + 1 > 4 * r' + r -> n = 2 * s' * (2 * s') + (4 * r' + r).
proof: Proof. intros; subst; ring. Qed.
imports: Arith ArithRing Lia