proposition: Lemma coord_exchange_axes : forall O E S U1 U2 P X Y, Cd O E S U1 U2 P X Y -> Cd O E S U2 U1 P Y X.
proof: Proof. intros O E S U1 U2 P X Y HCd. destruct HCd as [HCs [H [HPX HPY]]]; clear H. split; try (apply grid_exchange_axes; auto). split; try apply all_coplanar. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths