proposition: Lemma prop_21_1 : forall A B C D, OS A B C D -> OS B C A D -> OS A C B D -> LtA B A C B D C.
proof: Proof. apply os3__lta. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions