proposition: Lemma prop_19 : forall A B C, ~ Col A B C -> LtA B C A A B C -> LtA C A B A B C -> Lt A B A C /\ Lt B C A C.
proof: Proof. intros. split. - apply l11_44_2_b. Col. apply lta_left_comm; assumption. - apply lt_comm, l11_44_2_b. Col. apply lta_right_comm; assumption. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions