proposition: Lemma cong_cop_image__col : forall A B P P' X, P <> P' -> Reflect P P' A B -> Cong P X P' X -> Coplanar A B P X -> Col A B X.
proof: Proof. intros. unfold Reflect in *. induction H0. spliter. unfold ReflectL in H3. spliter. ex_and H3 M. induction H4. induction(eq_dec_points A M). subst M. assert (Perp P A A B). eapply perp_col. apply perp_distinct in H4. spliter. intro. subst P. apply l7_2 in H3. apply is_midpoint_id in H3. subst P'. absurde. apply perp_sym. apply perp_right_comm. apply H4. unfold Col. right; left. apply midpoint_bet. assumption. apply perp_comm in H6. apply perp_perp_in in H6. apply perp_in_comm in H6. apply perp_in_per in H6. assert (Per X A P). unfold Per. exists P'. split. apply l7_2. assumption. Cong. apply l8_2 in H6. apply col_permutation_2. apply (cop_per2__col P). Cop. intro. subst P. apply l7_2 in H3. apply is_midpoint_id in H3. subst P'. absurde. assumption. assumption. assert (Perp P M M A). eapply perp_col. intro. subst P. apply l7_2 in H3. apply is_midpoint_id in H3. subst P'. absurde. apply perp_sym. apply perp_comm. eapply perp_col. assumption. apply H4. assumption. unfold Col. right; left. apply midpoint_bet. assumption. apply perp_comm in H7. apply perp_perp_in in H7. apply perp_in_comm in H7. apply perp_in_per in H7. assert (Per X M P). unfold Per. exists P'. split. apply l7_2. assumption. apply cong_commutativity. assumption. apply l8_2 in H7. assert (Col A X M). assert (P <> M). intro. subst P. apply l7_2 in H3. apply is_midpoint_id in H3. subst P'. absurde. apply (cop_per2__col P). apply coplanar_perm_2, col_cop__cop with B; Cop. assumption. assumption. assumption. eapply col_transitivity_1. apply H6. apply col_permutation_5. assumption. apply col_permutation_5. assumption. subst P'. absurde. spliter;subst;Col. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity