proposition: Lemma add_sqrt_up_le : forall a b, 0<=a -> 0<=b -> √°a + √°b <= S √°(2*(a+b)).
proof: Proof. intros a b Ha Hb. le_elim Ha;[le_elim Hb|]. - rewrite 3 sqrt_up_eqn; trivial. + nzsimpl. rewrite <- 2 succ_le_mono. etransitivity; [eapply add_sqrt_le|]. * apply lt_succ_r. now rewrite (lt_succ_pred 0 a Ha). * apply lt_succ_r. now rewrite (lt_succ_pred 0 b Hb). * apply sqrt_le_mono. apply lt_succ_r. rewrite (lt_succ_pred 0). -- apply mul_lt_mono_pos_l. ++ order'. ++ apply add_lt_mono. ** apply le_succ_l. now rewrite (lt_succ_pred 0). ** apply le_succ_l. now rewrite (lt_succ_pred 0). -- apply mul_pos_pos. ++ order'. ++ now apply add_pos_pos. + apply mul_pos_pos. * order'. * now apply add_pos_pos. - rewrite <- Hb, sqrt_up_0. nzsimpl. apply le_le_succ_r, sqrt_up_le_mono. rewrite <- (mul_1_l a) at 1. apply mul_le_mono_nonneg_r; order'. - rewrite <- Ha, sqrt_up_0. nzsimpl. apply le_le_succ_r, sqrt_up_le_mono. rewrite <- (mul_1_l b) at 1. apply mul_le_mono_nonneg_r; order'. Qed.
imports: NZAxioms NZMulOrder