proposition: Lemma Par_perm : forall A B C D, Par A B C D -> Par A B C D /\ Par B A C D /\ Par A B D C /\ Par B A D C /\ Par C D A B /\ Par C D B A /\ Par D C A B /\ Par D C B A.
proof: Proof. intros. do 7 (split; Par). Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles