proposition: Lemma col_cop2_perp2__col : forall X1 X2 Y1 Y2 A B, Perp X1 X2 A B -> Perp Y1 Y2 A B -> Col X1 Y1 Y2 -> Coplanar A B X2 Y1 -> Coplanar A B X2 Y2 -> Col X2 Y1 Y2.
proof: Proof. intros. induction(eq_dec_points X1 Y2). subst Y2. assert(Perp Y1 X1 A B). eapply perp_col. intro. treat_equalities. apply perp_distinct in H0. intuition. apply H0. Col. apply col_permutation_1. apply cop_perp2__col with A B. assumption. apply H. apply perp_left_comm. assumption. assert(Perp Y2 X1 A B). eapply perp_col. auto. apply perp_left_comm. apply H0. Col. assert(Perp X1 Y2 A B). eapply perp_left_comm. assumption. induction(eq_dec_points X1 Y1). subst Y1. apply col_permutation_2. apply cop_perp2__col with A B; Cop. assert(Perp X1 Y1 A B). eauto using perp_left_comm, perp_col with col. assert (Col X1 X2 Y1). apply cop_perp2__col with A B; Perp; Cop. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles