proposition: Lemma l11_60_aux : forall A B C D P Q, ~ Col A B C -> Cong A P A Q -> Cong B P B Q -> Cong C P C Q -> Coplanar A B C D -> Cong D P D Q.
proof: Proof. intros A B C D P Q HNCol HA HB HC HCop. destruct (midpoint_existence P Q) as [M []]. assert_diffs; destruct HCop as [X [|[|]]]; spliter. - apply l4_17 with C X; Col. intro; subst; apply HNCol; assumption. apply l4_17 with A B; auto. - apply l4_17 with B X; Col. intro; subst; apply HNCol; Col. apply l4_17 with A C; auto. - apply l4_17 with A X; Col. intro; subst; apply HNCol; Col. apply l4_17 with B C; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2