proposition: Lemma isometric_trans_rot : forall x1 y1 x2 y2 tx ty theta:R, Rsqr (x1 - x2) + Rsqr (y1 - y2) = Rsqr (xt (xr x1 y1 theta) tx - xt (xr x2 y2 theta) tx) + Rsqr (yt (yr x1 y1 theta) ty - yt (yr x2 y2 theta) ty).
proof: Proof. intros; rewrite <- isometric_translation; apply isometric_rotation_0. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt