proposition: Lemma image_preserves_bet1 : forall X Y A B C A' B' C', Bet A B C -> Reflect A A' X Y -> Reflect B B' X Y -> Reflect C C' X Y -> Bet A' B' C'.
proof: Proof. intros. induction(eq_dec_points X Y). subst Y. unfold Reflect in *. induction H0. tauto. induction H1. tauto. induction H2. tauto. spliter. clean_duplicated_hyps. apply(l7_15 A B C A' B' C' X). apply l7_2. auto. apply l7_2; auto. apply l7_2; auto. assumption. apply (image_preserves_bet A B C A' B' C' X Y). unfold Reflect in H0. induction H0. tauto. spliter. contradiction. unfold Reflect in *. induction H0; induction H1; induction H2; try( spliter; contradiction). spliter. auto. induction H0; induction H1; induction H2; try( spliter; contradiction). spliter. auto. induction H0; induction H1; induction H2; try( spliter; contradiction). spliter. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order