proposition: Lemma isometric_rotation : forall x1 y1 x2 y2 theta:R, dist_euc x1 y1 x2 y2 = dist_euc (xr x1 y1 theta) (yr x1 y1 theta) (xr x2 y2 theta) (yr x2 y2 theta).
proof: Proof. unfold dist_euc; intros; apply Rsqr_inj; [ apply sqrt_positivity; apply Rplus_le_le_0_compat | apply sqrt_positivity; apply Rplus_le_le_0_compat | repeat rewrite Rsqr_sqrt; [ apply isometric_rotation_0 | apply Rplus_le_le_0_compat | apply Rplus_le_le_0_compat ] ]; apply Rle_0_sqr. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt