proposition: Lemma l4_14 : forall A B C A' B', Col A B C -> Cong A B A' B' -> exists C', Cong_3 A B C A' B' C'.
proof: Proof. unfold Col. intros. intuition. prolong A' B' C' B C. exists C'. assert (Cong A C A' C') by (eapply l2_11;eCong). unfold Cong_3;intuition. assert (exists C', Bet A' C' B' /\ Cong_3 A C B A' C' B') by (eapply l4_5;Between). ex_and H1 C'. exists C'. auto with cong3. prolong B' A' C' A C. exists C'. assert (Cong B C B' C') by (eapply l2_11;eBetween;Cong). unfold Cong_3;intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch04_cong_bet