proposition: Lemma sqrt_up_succ_le : forall a, 0<=a -> √°(S a) <= S (√°a).
proof: Proof. intros a Ha. apply sqrt_up_le_square. - now apply le_le_succ_r. - apply le_le_succ_r, sqrt_up_nonneg. - rewrite <- (add_1_l (√°a)). apply le_trans with (1²+(√°a)²). + rewrite mul_1_l, add_1_l, <- succ_le_mono. now apply sqrt_sqrt_up_spec. + apply add_square_le. * order'. * apply sqrt_up_nonneg. Qed.
imports: NZAxioms NZMulOrder