proposition: Lemma par_cong_plg : forall A B C D, Par A B C D -> Cong A B C D -> Plg A B C D \/ Plg A B D C.
proof: Proof. intros A B C D HPar HCong. destruct (par_cong_mid A B C D) as [M HM]; trivial. elim HM; clear HM; intro HM; destruct HM as [HMid1 HMid2]. { left; split; [|exists M; split; assumption]. destruct (eq_dec_points A C); [|left; assumption]. apply par_distinct in HPar. right; intro; treat_equalities; apply HPar; reflexivity. } { right; split; [|exists M; split; assumption]. destruct (eq_dec_points A D); [|left; assumption]. apply par_distinct in HPar. right; intro; treat_equalities; apply HPar; reflexivity. } Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates