proposition: Lemma isometric_translation : forall x1 x2 y1 y2 tx ty:R, Rsqr (x1 - x2) + Rsqr (y1 - y2) = Rsqr (xt x1 tx - xt x2 tx) + Rsqr (yt y1 ty - yt y2 ty).
proof: Proof. intros; unfold Rsqr, xt, yt; ring. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt