proposition: Lemma sqrt_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_neg a Ha). nzsimpl. apply sqrt_le_mono. rewrite <- (add_0_l b) at 2. apply add_le_mono_r; order. - intros a b. destruct (lt_ge_cases a 0) as [Ha|Ha]. + now apply AUX. + destruct (lt_ge_cases b 0) as [Hb|Hb]. * rewrite (add_comm a), (add_comm (√a)); now apply AUX. * assert (Ha':=sqrt_nonneg a). assert (Hb':=sqrt_nonneg b). rewrite <- lt_succ_r. apply sqrt_lt_square. -- now apply add_nonneg_nonneg. -- now apply lt_le_incl, lt_succ_r, add_nonneg_nonneg. -- destruct (sqrt_spec a Ha) as (_,LTa). destruct (sqrt_spec b Hb) as (_,LTb). revert LTa LTb. nzsimpl. rewrite 3 lt_succ_r. intros LTa LTb. assert (H:=add_le_mono _ _ _ _ LTa LTb). etransitivity; [eexact H|]. clear LTa LTb H. rewrite <- (add_assoc _ (√a) (√a)). rewrite <- (add_assoc _ (√b) (√b)). rewrite add_shuffle1. rewrite <- (add_assoc _ (√a + √b)). rewrite (add_shuffle1 (√a) (√b)). apply add_le_mono_r. now apply add_square_le. Qed.
imports: NZAxioms NZMulOrder