proposition: Theorem bsqrt_exact : forall b n:nat, n <= b -> let (s, r) := bsqrt n b in n = s * s + r.
proof: Proof. intros b; elim b. intros n Hle; rewrite (proj1 (Nat.le_0_r _) Hle); simpl in |- *; auto. intros b' Hrec n Hle; cbv beta iota zeta delta [bsqrt] in |- *; fold bsqrt in |- *. generalize (div4_lt n) (div4_exact n). case (div4 n). intros q r; case q. - case r; intros; subst; ring. - intros q' Hlt Heq; generalize (Hrec (S q')); case (bsqrt (S q') b'). intros s' r' Hrec'. case (le_gt_dec (4 * s' + 1) (4 * r' + r)). apply bsqrt_exact_lemma_le with (S q'); auto; lia. apply bsqrt_exact_lemma_gt with (S q'); auto; lia. Qed.
imports: Arith ArithRing Lia