proposition: Lemma triangle_rectangle_lt : 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_lt_is_lt (Rsqr x) (Rsqr y) (Rsqr z) (Rle_0_sqr y) H); intro; apply Rsqr_lt_abs_0; assumption | rewrite Rplus_comm in H; generalize (plus_lt_is_lt (Rsqr y) (Rsqr x) (Rsqr z) (Rle_0_sqr x) H); intro; apply Rsqr_lt_abs_0; assumption ]. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun