proposition: Lemma par_strict_symmetry :forall A B C D, Par_strict A B C D -> Par_strict C D A B.
proof: Proof. unfold Par_strict. intros. spliter. split. apply coplanar_perm_16;assumption. intro. apply H0. ex_and H1 X. exists X. split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles