proposition: Lemma isometric_rotation_0 : forall x1 y1 x2 y2 theta:R, Rsqr (x1 - x2) + Rsqr (y1 - y2) = Rsqr (xr x1 y1 theta - xr x2 y2 theta) + Rsqr (yr x1 y1 theta - yr x2 y2 theta).
proof: Proof. intros; unfold xr, yr; replace (x1 * cos theta + y1 * sin theta - (x2 * cos theta + y2 * sin theta)) with (cos theta * (x1 - x2) + sin theta * (y1 - y2)); [ replace (- x1 * sin theta + y1 * cos theta - (- x2 * sin theta + y2 * cos theta)) with (cos theta * (y1 - y2) + sin theta * (x2 - x1)); [ repeat rewrite Rsqr_plus; repeat rewrite Rsqr_mult; repeat rewrite cos2; ring_simplify; replace (x2 - x1) with (- (x1 - x2)); [ rewrite <- Rsqr_neg; ring | ring ] | ring ] | ring ]. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt