proposition: Lemma par_strict_right_comm : forall A B C D, Par_strict A B C D -> Par_strict A B D C.
proof: Proof. unfold Par_strict. intros. decompose [and] H;clear H. split. apply coplanar_perm_1;assumption. intro. apply H1. ex_and H X. exists X; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles