proposition: Lemma add_sqrt_le : forall a b, 0<=a -> 0<=b -> √a + √b <= √(2*(a+b)).
proof: Proof. intros a b Ha Hb. assert (Ha':=sqrt_nonneg a). assert (Hb':=sqrt_nonneg b). apply sqrt_le_square. - apply mul_nonneg_nonneg. + order'. + now apply add_nonneg_nonneg. - now apply add_nonneg_nonneg. - transitivity (2*((√a)² + (√b)²)). + now apply square_add_le. + apply mul_le_mono_nonneg_l. * order'. * apply add_le_mono; now apply sqrt_spec. Qed.
imports: NZAxioms NZMulOrder