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