proposition: Lemma bet_cong3 : forall A B C A' B', Bet A B C -> Cong A B A' B' -> exists C', Cong_3 A B C A' B' C'.
proof: Proof. intros. assert (exists x, Bet A' B' x /\ Cong B' x B C) by (apply segment_construction). ex_and H1 x. assert (Cong A C A' x). eapply l2_11. apply H. apply H1. assumption. Cong. exists x;unfold Cong_3; repeat split;Cong. Qed.
imports: GeoCoq.Tarski_dev.Definitions GeoCoq.Tactics.finish