proposition: Lemma sqrt_up_mul_above : forall a b, 0<=a -> 0<=b -> √°(a*b) <= √°a * √°b.
proof: Proof. intros a b Ha Hb. apply sqrt_up_le_square. - now apply mul_nonneg_nonneg. - apply mul_nonneg_nonneg; apply sqrt_up_nonneg. - rewrite mul_shuffle1. apply mul_le_mono_nonneg; trivial; now apply sqrt_sqrt_up_spec. Qed.
imports: NZAxioms NZMulOrder