proposition: Lemma image_preserves_col : forall X Y A B C A' B' C', Col A B C -> Reflect A A' X Y -> Reflect B B' X Y -> Reflect C C' X Y -> Col A' B' C'.
proof: Proof. intros. induction H. unfold Col. left. apply (image_preserves_bet1 X Y A B C A' B' C'); auto. induction H. unfold Col. right; left. apply (image_preserves_bet1 X Y B C A B' C' A'); auto. unfold Col. right; right. apply (image_preserves_bet1 X Y C A B C' A' B'); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order