proposition: Lemma prop_15 : forall A B C D E, Bet A E B -> A <> E -> B <> E -> Bet C E D -> C <> E -> D <> E -> CongA A E C B E D.
proof: Proof. intros. apply l11_14; auto. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions