proposition: Lemma sqrt_up_add_le : forall a b, √°(a+b) <= √°a + √°b.
proof: Proof. assert (AUX : forall a b, a<=0 -> √°(a+b) <= √°a + √°b). - intros a b Ha. rewrite (sqrt_up_eqn0 a Ha). nzsimpl. apply sqrt_up_le_mono. rewrite <- (add_0_l b) at 2. apply add_le_mono_r; order. - intros a b. destruct (le_gt_cases a 0) as [Ha|Ha]. + now apply AUX. + destruct (le_gt_cases b 0) as [Hb|Hb]. * rewrite (add_comm a), (add_comm (√°a)); now apply AUX. * rewrite 2 sqrt_up_eqn; trivial. -- nzsimpl. rewrite <- succ_le_mono. transitivity (√(P a) + √b). ++ rewrite <- (lt_succ_pred 0 a Ha) at 1. nzsimpl. apply sqrt_add_le. ++ apply add_le_mono_l. apply le_sqrt_sqrt_up. -- now apply add_pos_pos. Qed.
imports: NZAxioms NZMulOrder