proposition: Lemma projp_preserves_bet : forall A B C A' B' C' X Y, Bet A B C -> Projp A A' X Y -> Projp B B' X Y -> Projp C C' X Y -> Bet A' B' C'.
proof: Proof. intros. eapply projp_is_project_perp in H0. ex_and H0 T. ex_and H3 U. eapply (project_preserves_bet X Y T U A B C A' B' C'). apply H. assumption. eapply projp_to_project in H1. apply H1. assumption. eapply projp_to_project in H2. apply H2. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors