proposition: Lemma l9_33 : forall A B C D, Copl A B C D <-> Coplanar A B C D.
proof: Proof. intros A B C D; split; [intros [E [F [G]]]; spliter|intro HCop]; [apply coplanar_pseudo_trans with E F G; auto; apply InPlane'__Coplanar; auto|]. assert (HE : forall A B C D, A <> B -> Coplanar A B C D -> Copl A B C D). { clear -TnEQD; intros A B C D HAB HCop. elim (col_dec A B C); intro HABC; elim (col_dec A B D); intro HABD. { destruct (not_col_exists A B) as [E]; auto. exists A, B, E; repeat split; auto; left; Col. } { exists A, B, D; repeat split; auto; [left..|right; left; apply one_side_reflexivity]; Col. } { exists A, B, C; repeat split; auto; [left..|right; left; apply one_side_reflexivity|left]; Col. } { exists A, B, C; repeat split; auto; [left..|right; left; apply one_side_reflexivity|]; Col. destruct (cop__one_or_two_sides A B C D); Col; right; [right|left]; auto. } } elim (eq_dec_points A B); intro; [|cut (Copl A B C D); [Copl'|apply HE; Cop]]. elim (eq_dec_points A C); intro; [|cut (Copl A C B D); [Copl'|apply HE; Cop]]. elim (eq_dec_points A D); intro; [|cut (Copl A D B C); [Copl'|apply HE; Cop]]. elim (eq_dec_points B C); intro; [|cut (Copl B C A D); [Copl'|apply HE; Cop]]. elim (eq_dec_points B D); intro; [|cut (Copl B D A C); [Copl'|apply HE; Cop]]. elim (eq_dec_points C D); intro; [|cut (Copl C D A B); [Copl'|apply HE; Cop]]. subst B; subst C; subst D; destruct (another_point A) as [B]. destruct (not_col_exists A B) as [C]; auto. exists A, B, C; repeat split; [|left..]; Col. Qed.
imports: GeoCoq.Tarski_dev.Annexes.coplanar GeoCoq.Tarski_dev.Ch09_plane