proposition: Lemma triangle_rectangle_le : forall x y z:R, Rsqr x + Rsqr y <= Rsqr z -> Rabs x <= Rabs z /\ Rabs y <= Rabs z.
proof: Proof. intros; split; [ generalize (plus_le_is_le (Rsqr x) (Rsqr y) (Rsqr z) (Rle_0_sqr y) H); intro; apply Rsqr_le_abs_0; assumption | rewrite Rplus_comm in H; generalize (plus_le_is_le (Rsqr y) (Rsqr x) (Rsqr z) (Rle_0_sqr x) H); intro; apply Rsqr_le_abs_0; assumption ]. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun