proposition: Lemma sqrt_succ_le : forall a, 0<=a -> √(S a) <= S (√a).
proof: Proof. intros a Ha. apply lt_succ_r. apply sqrt_lt_square. - now apply le_le_succ_r. - apply le_le_succ_r, le_le_succ_r, sqrt_nonneg. - rewrite <- (add_1_l (S (√a))). apply lt_le_trans with (1²+(S (√a))²). + rewrite mul_1_l, add_1_l, <- succ_lt_mono. now apply sqrt_spec. + apply add_square_le. * order'. * apply le_le_succ_r, sqrt_nonneg. Qed.
imports: NZAxioms NZMulOrder