proposition: Lemma l9_30 : forall A B C D E F P X Y Z, ~ Coplanar A B C P -> ~ Col D E F -> Coplanar D E F P -> Coplanar A B C X -> Coplanar A B C Y -> Coplanar A B C Z -> Coplanar D E F X -> Coplanar D E F Y -> Coplanar D E F Z -> Col X Y Z.
proof: Proof. intros A B C D E F P X Y Z HNCop HNCol HP HX1 HY1 HZ1 HX2 HY2 HZ2. destruct (col_dec X Y Z); [assumption|]. assert (~ Col A B C) by (apply ncop__ncol with P, HNCop). exfalso. apply HNCop. apply coplanar_pseudo_trans with X Y Z; [assumption|apply coplanar_pseudo_trans with A B C; Cop..|]; apply coplanar_pseudo_trans with D E F; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar