proposition: Lemma cop_image_in2__col : forall A B P P' Q Q' M, Coplanar A B P Q -> ReflectL_at M P P' A B -> ReflectL_at M Q Q' A B -> Col M P Q.
proof: Proof. intros. assert(ReflectL P P' A B). eapply (image_in_is_image_spec M). assumption. assert(ReflectL Q Q' A B). eapply (image_in_is_image_spec M). assumption. unfold ReflectL_at in *. spliter. induction H4. induction H6. induction (eq_dec_points A M). subst M. assert (Per B A P). unfold Per. exists P'. split. apply l7_2. assumption. apply cong_commutativity. eapply is_image_spec_col_cong with A B;Col. assert (Per B A Q). unfold Per. exists Q'. split. apply l7_2. assumption. apply cong_commutativity. eapply is_image_spec_col_cong with A B;Col. apply col_permutation_2. apply cop_per2__col with B. Cop. apply perp_distinct in H4. spliter. auto. apply l8_2. apply H8. apply l8_2. assumption. assert (Per A M P). unfold Per. exists P'. split. apply l7_2. assumption. apply cong_commutativity. eapply is_image_spec_col_cong. apply H2. Col. assert (Per A M Q). unfold Per. exists Q'. split. apply l7_2. assumption. apply cong_commutativity. eapply is_image_spec_col_cong. apply H3. apply col_trivial_3. apply col_permutation_2. apply cop_per2__col with A. assert_diffs; apply coplanar_perm_12, col_cop__cop with B; Cop. auto. apply l8_2. apply H9. auto. apply l8_2. assumption. subst P'. apply l7_3 in H0. subst P. Col. subst Q'. apply l7_3 in H1. subst Q. Col. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity