proposition: Lemma sqrt_mul_above : forall a b, 0<=a -> 0<=b -> √(a*b) < S (√a) * S (√b).
proof: Proof. intros a b Ha Hb. apply sqrt_lt_square. - now apply mul_nonneg_nonneg. - apply mul_nonneg_nonneg. + now apply lt_le_incl, lt_succ_r, sqrt_nonneg. + now apply lt_le_incl, lt_succ_r, sqrt_nonneg. - rewrite mul_shuffle1. apply mul_lt_mono_nonneg; trivial; now apply sqrt_spec. Qed.
imports: NZAxioms NZMulOrder