proposition: Lemma distance_refl : forall x0 y0:R, dist_euc x0 y0 x0 y0 = 0.
proof: Proof. intros x0 y0; unfold dist_euc; apply Rsqr_inj; [ apply sqrt_positivity; apply Rplus_le_le_0_compat; [ apply Rle_0_sqr | apply Rle_0_sqr ] | right; reflexivity | rewrite Rsqr_0; rewrite Rsqr_sqrt; [ unfold Rsqr; ring | apply Rplus_le_le_0_compat; [ apply Rle_0_sqr | apply Rle_0_sqr ] ] ]. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt