proposition: Lemma par_left_comm : forall A B C D, Par A B C D -> Par B A C D.
proof: Proof. unfold Par. intros. induction H. left. apply par_strict_left_comm; assumption. right. spliter. Col5. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles