proposition: Lemma par_symmetry :forall A B C D, Par A B C D -> Par C D A B.
proof: Proof. unfold Par. intros. induction H. left. apply par_strict_symmetry. assumption. spliter. right. repeat split; try assumption. eapply (col_transitivity_1 _ D);Col. eapply (col_transitivity_1 _ C);Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles