proposition: Lemma sqrt_up_succ_square : forall a, 0<=a -> √°(S a²) == S a.
proof: Proof. intros a Ha. rewrite sqrt_up_eqn by (now apply lt_succ_r, mul_nonneg_nonneg). now rewrite pred_succ, sqrt_square. Qed.
imports: NZAxioms NZMulOrder