proposition: Lemma prop_16 : forall A B C D, ~ Col A B C -> Bet B C D -> C <> D -> LtA C A B A C D /\ LtA C B A A C D.
proof: Proof. intros. apply l11_41; Col. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions