proposition: Lemma sqrt_eq_succ_iff_square : forall a, 0<=a -> (√(S a) == S (√a) <-> exists b, 0<b /\ S a == b²).
proof: Proof. intros a Ha. split. - intros EQ. exists (S (√a)). split. + apply lt_succ_r, sqrt_nonneg. + generalize (proj2 (sqrt_spec a Ha)). rewrite <- le_succ_l. assert (Ha' : 0 <= S a) by now apply le_le_succ_r. generalize (proj1 (sqrt_spec (S a) Ha')). rewrite EQ; order. - intros (b & Hb & H). rewrite H. rewrite sqrt_square; try order. symmetry. rewrite <- (lt_succ_pred 0 b Hb). f_equiv. rewrite <- (lt_succ_pred 0 b²) in H. + apply succ_inj in H. now rewrite H, sqrt_pred_square. + now apply mul_pos_pos. Qed.
imports: NZAxioms NZMulOrder