proposition: Lemma sqrt_up_mul_below : forall a b, 0<a -> 0<b -> (P √°a)*(P √°b) < √°(a*b).
proof: Proof. intros a b Ha Hb. apply sqrt_up_lt_square. - apply mul_nonneg_nonneg; order. - apply mul_nonneg_nonneg; apply lt_succ_r. + rewrite (lt_succ_pred 0); now rewrite sqrt_up_pos. + rewrite (lt_succ_pred 0); now rewrite sqrt_up_pos. - rewrite mul_shuffle1. apply mul_lt_mono_nonneg; trivial using square_nonneg; now apply sqrt_up_spec. Qed.
imports: NZAxioms NZMulOrder