proposition: Lemma par_cong_cop : forall A B C D, Par A B C D -> Cong A B C D -> Coplanar A B C D.
proof: Proof. intros. destruct (par_cong_mid A B C D) as [M HM]; trivial. exists M; right. destruct HM as [[]|[]]; [left|right]; split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates