proposition: Lemma image_gen_preserves_inter : forall A B C D I A' B' C' D' I' X Y, Reflect A A' X Y -> Reflect B B' X Y -> Reflect C C' X Y -> Reflect D D' X Y -> ~ Col A B C -> C <> D -> Col A B I -> Col C D I -> Col A' B' I' -> Col C' D' I' -> Reflect I I' X Y.
proof: Proof. intros. destruct (l10_6_existence X Y I) as [I0 HI0]; trivial. assert (I' = I0); [|subst; assumption]. apply (l6_21 A' B' C' D'); trivial. apply image_gen_preserves_ncol with A B C X Y; assumption. intro; subst D'; apply H4, l10_2_uniqueness with X Y C'; assumption. apply image_gen_preserves_col with A B I X Y; assumption. apply image_gen_preserves_col with C D I X Y; assumption. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity