proposition: Lemma par_strict_comm : forall A B C D, Par_strict A B C D -> Par_strict B A D C.
proof: Proof. intros. apply par_strict_left_comm in H. apply par_strict_right_comm. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles