proposition: Lemma col_perp2_ncol__col : forall X1 X2 Y1 Y2 A B, Perp X1 X2 A B -> Perp Y1 Y2 A B -> Col X1 Y1 Y2 -> ~ Col X1 A B -> Col X2 Y1 Y2.
proof: Proof. intros. assert (Coplanar A B X2 Y1). induction (eq_dec_points X1 Y1). subst; Cop. apply coplanar_trans_1 with X1; [Cop..|]. assert (Perp Y1 X1 A B) by (apply perp_col with Y2; Col); Cop. assert (Coplanar A B X2 Y2). induction (eq_dec_points X1 Y2). subst; Cop. apply coplanar_trans_1 with X1; [Cop..|]. assert (Perp Y2 X1 A B) by (apply perp_col with Y1; Perp; Col); Cop. apply col_cop2_perp2__col with X1 A B; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles