proposition: Theorem bsqrt_rem : forall b n:nat, n <= b -> let (s, r) := bsqrt n b in n < (s + 1) * (s + 1).
proof: Proof. intros b; elim b. - intros n Hle; rewrite (proj1 (Nat.le_0_r _) Hle); simpl in |- *; auto with arith. - intros b' Hrec n Hle; generalize (bsqrt_exact (S b') n Hle); cbv beta iota zeta delta [bsqrt] in |- *; fold bsqrt in |- *. generalize (div4_lt n) (div4_exact n) (div4_lt_rem n). case (div4 n); intros q r; case q. + case r; intros; subst; simpl in |- *; auto with arith. + intros q' Hlt Heq Hlt_rem; generalize (Hrec (S q')). case (bsqrt (S q') b'). intros s' r' Hrec'. case (le_gt_dec (4 * s' + 1) (4 * r' + r)). * intros Hle' Heq'; rewrite Heq. apply Nat.lt_le_trans with (4 * S q' + 4). auto with arith. replace ((2 * s' + 1 + 1) * (2 * s' + 1 + 1)) with (4 * ((s' + 1) * (s' + 1))). abstract lia. ring. * intros Hgt Heq'; rewrite Heq'. match goal with | |- (?X1 < ?X2) => ring_simplify X1; ring_simplify X2 end. abstract lia. Qed.
imports: Arith ArithRing Lia