proposition: Lemma Par_cases : forall 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 -> Par A B C D.
proof: Proof. intros. decompose [or] H;Par. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles