proposition: Lemma sqrt_up_eq_succ_iff_square : forall a, 0<=a -> (√°(S a) == S (√°a) <-> exists b, 0<=b /\ a == b²).
proof: Proof. intros a Ha. split. - intros EQ. le_elim Ha. + exists (√°a). split. * apply sqrt_up_nonneg. * generalize (proj2 (sqrt_up_spec a Ha)). assert (Ha' : 0 < S a) by (apply lt_succ_r; order'). generalize (proj1 (sqrt_up_spec (S a) Ha')). rewrite EQ, pred_succ, lt_succ_r. order. + exists 0. nzsimpl. now split. - intros (b & Hb & H). now rewrite H, sqrt_up_succ_square, sqrt_up_square. Qed.
imports: NZAxioms NZMulOrder