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