proposition: Lemma image_gen_preserves_ncol : forall A B C A' B' C' X Y, Reflect A A' X Y -> Reflect B B' X Y -> Reflect C C' X Y -> ~ Col A B C -> ~ Col A' B' C'.
proof: Proof. intros. intro. apply H2, image_gen_preserves_col with A' B' C' X Y; try (apply l10_4); assumption. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity