proposition: Lemma symmetry_preserves_per : forall A P B A' P', Per B P A -> Midpoint B A A' -> Midpoint B P P' -> Per B P' A'.
proof: Proof. intros. assert(HS:=symmetric_point_construction A P). ex_and HS C. assert(HS:=symmetric_point_construction C B). ex_and HS C'. assert(HH:= symmetry_preserves_midpoint A P C A' P' C' B H0 H1 H3 H2). unfold Per. exists C'. split. assumption. unfold Per in H. ex_and H X. assert(X = C). apply(symmetric_point_uniqueness A P X C); auto. subst X. unfold Midpoint in *. spliter. apply (cong_transitivity _ _ B A). Cong. apply(cong_transitivity _ _ B C). assumption. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel