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