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