proposition: Lemma prop_9 : forall A B C, A <> B -> A <> C -> exists F, InAngle F B A C /\ CongA F A B F A C.
proof: Proof. intros. apply angle_bisector; auto. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions