proposition: Lemma triangle : forall x0 y0 x1 y1 x2 y2:R, dist_euc x0 y0 x1 y1 <= dist_euc x0 y0 x2 y2 + dist_euc x2 y2 x1 y1.
proof: Proof. intros; unfold dist_euc; apply Rsqr_incr_0; [ rewrite Rsqr_plus; repeat rewrite Rsqr_sqrt; [ replace (Rsqr (x0 - x1)) with (Rsqr (x0 - x2) + Rsqr (x2 - x1) + 2 * (x0 - x2) * (x2 - x1)); [ replace (Rsqr (y0 - y1)) with (Rsqr (y0 - y2) + Rsqr (y2 - y1) + 2 * (y0 - y2) * (y2 - y1)); [ apply Rplus_le_reg_l with (- Rsqr (x0 - x2) - Rsqr (x2 - x1) - Rsqr (y0 - y2) - Rsqr (y2 - y1)); replace (- Rsqr (x0 - x2) - Rsqr (x2 - x1) - Rsqr (y0 - y2) - Rsqr (y2 - y1) + (Rsqr (x0 - x2) + Rsqr (x2 - x1) + 2 * (x0 - x2) * (x2 - x1) + (Rsqr (y0 - y2) + Rsqr (y2 - y1) + 2 * (y0 - y2) * (y2 - y1)))) with (2 * ((x0 - x2) * (x2 - x1) + (y0 - y2) * (y2 - y1))); [ replace (- Rsqr (x0 - x2) - Rsqr (x2 - x1) - Rsqr (y0 - y2) - Rsqr (y2 - y1) + (Rsqr (x0 - x2) + Rsqr (y0 - y2) + (Rsqr (x2 - x1) + Rsqr (y2 - y1)) + 2 * sqrt (Rsqr (x0 - x2) + Rsqr (y0 - y2)) * sqrt (Rsqr (x2 - x1) + Rsqr (y2 - y1)))) with (2 * (sqrt (Rsqr (x0 - x2) + Rsqr (y0 - y2)) * sqrt (Rsqr (x2 - x1) + Rsqr (y2 - y1)))); [ apply Rmult_le_compat_l; [ left; cut (0%nat <> 2%nat); [ intros; generalize (lt_INR_0 2 (proj1 (Nat.neq_0_lt_0 2) (Nat.neq_sym 0 2 H))); intro H0; assumption | discriminate ] | apply sqrt_cauchy ] | ring ] | ring ] | ring_Rsqr ] | ring_Rsqr ] | apply Rplus_le_le_0_compat; apply Rle_0_sqr | apply Rplus_le_le_0_compat; apply Rle_0_sqr | apply Rplus_le_le_0_compat; apply Rle_0_sqr ] | apply sqrt_positivity; apply Rplus_le_le_0_compat; apply Rle_0_sqr | apply Rplus_le_le_0_compat; apply sqrt_positivity; apply Rplus_le_le_0_compat; apply Rle_0_sqr ]. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt