proposition: Lemma image_gen_preserves_col : 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. destruct H2 as [HBet|[HBet|HBet]]; [|apply col_permutation_2|apply col_permutation_1]; apply bet_col; eapply image_gen_preserves_bet; eauto. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity