proposition: Lemma cop4_perp_in2__col : forall A B A' B' X Y P, Coplanar X Y A A' -> Coplanar X Y A B' -> Coplanar X Y B A' -> Coplanar X Y B B' -> Perp_at P A B X Y -> Perp_at P A' B' X Y -> Col A B A'.
proof: Proof. intros. assert(HP1:= H3). assert(HP2:=H4). assert(Col A B P /\ Col X Y P). apply perp_in_col in H3. spliter. split; Col. spliter. unfold Perp_at in H3. unfold Perp_at in H4. spliter. induction(eq_dec_points A P); induction(eq_dec_points P X). subst A. subst X. assert(Per B P Y). apply(H14 B Y); Col. assert(Per A' P Y). apply(H10 A' Y); Col. apply col_permutation_2. apply cop_per2__col with Y; Cop. subst A. assert(Per B P X). apply(H14 B X); Col. assert(Per A' P X). apply(H10 A' X); Col. apply col_permutation_2. apply cop_per2__col with X; auto. apply coplanar_perm_12. apply col_cop__cop with Y; Col; Cop. subst X. assert(Per A P Y). apply(H14 A Y); Col. induction(eq_dec_points P A'). subst A'. assert(Per B' P Y). apply(H10 B' Y); Col. assert(Col A B' P). apply cop_per2__col with Y; Cop. ColR. assert(Per A' P Y). apply(H10 A' Y); Col. assert(Col A A' P). apply cop_per2__col with Y; Cop. ColR. assert(Per A P X). apply(H14 A X); Col. induction(eq_dec_points P A'). subst A'. assert(Per B' P X). apply(H10 B' X); Col. assert(Col A B' P). apply cop_per2__col with X; auto. apply coplanar_perm_12. apply col_cop__cop with Y; Col; Cop. ColR. assert(Per A' P X). apply(H10 A' X); Col. assert(Col A A' P). apply cop_per2__col with X; auto. apply coplanar_perm_12. apply col_cop__cop with Y; Col; Cop. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel