proposition: Lemma add_square_le : forall a b, 0<=a -> 0<=b -> a*a + b*b <= (a+b)*(a+b).
proof: Proof. intros a b Ha Hb. rewrite mul_add_distr_r, !mul_add_distr_l. rewrite add_assoc. apply add_le_mono_r. rewrite <- add_assoc. rewrite <- (add_0_r (a*a)) at 1. apply add_le_mono_l. apply add_nonneg_nonneg; now apply mul_nonneg_nonneg. Qed.
imports: NZAxioms NZAddOrder