proposition: Lemma sqrt_mul_below : forall a b, √a * √b <= √(a*b).
proof: Proof. intros a b. destruct (lt_ge_cases a 0) as [Ha|Ha]. - rewrite (sqrt_neg a Ha). nzsimpl. apply sqrt_nonneg. - destruct (lt_ge_cases b 0) as [Hb|Hb]. + rewrite (sqrt_neg b Hb). nzsimpl. apply sqrt_nonneg. + assert (Ha':=sqrt_nonneg a). assert (Hb':=sqrt_nonneg b). apply sqrt_le_square; try now apply mul_nonneg_nonneg. rewrite mul_shuffle1. apply mul_le_mono_nonneg; try now apply mul_nonneg_nonneg. * now apply sqrt_spec. * now apply sqrt_spec. Qed.
imports: NZAxioms NZMulOrder