proposition: Lemma prop_14 : forall A B C D P Q R S T U, TS A B C D -> Per P Q R -> SumA A B C A B D S T U -> SumA P Q R P Q R S T U -> Bet C B D.
proof: Proof. intros A B C D P Q R S T U HTS HP HSuma1 HSuma2. apply (bet_conga__bet S T U). apply (per2_suma__bet P Q R P Q R); assumption. apply (suma2__conga A B C A B D). assumption. apply suma_left_comm, ts__suma, HTS. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions