proposition: Lemma Cop__Coplanar : forall A B C D, Cop A B C D <-> Coplanar A B C D.
proof: Proof. intros A B C D; split; [intros [E [F [G]]]; spliter|intros [X HX]]; [apply coplanar_pseudo_trans with E F G; auto; apply InPlane__Coplanar; auto|]. assert (HE : forall A B C D, Col A B X -> Col C D X -> Cop A B C D). { clear -TnEQD; intros A B C D HC1 HC2. elim (eq_dec_points A B); intro HAB; [subst; apply Cop_aabc|]. assert (HE : forall A B C D, (Col A B C /\ Col A B D) \/ ~ (Col A B C /\ Col A B D)). { clear -TnEQD; intros A B C D. elim (col_dec A B C); elim (col_dec A B D); tauto. } elim (HE A B C D); [intros [HC3 HC4]|]; clear HE. { assert (HY : exists Y, X <> Y /\ Col X Y A /\ Col X Y B /\ Col X Y C /\ Col X Y D). { elim (eq_dec_points A X); intro; [|exists A; repeat split; ColR]. elim (eq_dec_points B X); intro; [|exists B; repeat split; ColR]. subst A; subst B; exfalso; intuition. } destruct HY as [Y]; spliter. destruct (not_col_exists X Y) as [Z]; auto. exists X, Y, Z; repeat split; [|exists A|exists B|exists C|exists D]; Col. } { intro HC; assert (HNC : ~ Col A B C \/ ~ Col A B D); [elim (col_dec A B C); elim (col_dec A B D); tauto|clear HC]. destruct HNC as [HNC|HNC]; [exists A, B, C|exists A, B, D]; repeat split; Col; try solve [exists A; Col]; try solve [exists B; Col]; try solve [exists X; Col]. } } destruct HX as [[]|HX]; [cut (Cop A B C D); [Copl|apply HE; Col]|]. destruct HX as [[]|HX]; [cut (Cop A C B D); [Copl|apply HE; Col]|]. destruct HX as []; cut (Cop A D B C); [Copl|apply HE; Col]. Qed.
imports: GeoCoq.Tarski_dev.Annexes.coplanar GeoCoq.Tarski_dev.Ch09_plane