proposition: Lemma intersection_with_image_gen : forall A B C A' B' X Y, Reflect A A' X Y -> Reflect B B' X Y -> ~ Col A B A' -> Col A B C -> Col A' B' C -> Col C X Y.
proof: Proof. intros. apply l10_8. assert (Reflect A' A X Y) by (apply l10_4; assumption). assert (~ Col A' B' A) by (apply image_gen_preserves_ncol with A B A' X Y; trivial). assert_diffs. apply image_gen_preserves_inter with A B A' B' A' B' A B; trivial. apply l10_4; assumption. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity