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