proposition: Lemma conga_ex_cong3 : forall A B C A' B' C', CongA A B C A' B' C' -> exists AA, exists CC, Out B A AA -> Out B C CC -> Cong_3 AA B CC A' B' C'.
proof: Proof. intros. assert(B <> A /\ B <> C /\ B' <> A' /\ B' <> C'). unfold CongA in H. spliter. repeat split; auto. spliter. assert(exists AA, Out B A AA /\ Cong B AA B' A'). apply segment_construction_3; assumption. assert(exists CC, Out B C CC /\ Cong B CC B' C'). apply segment_construction_3; assumption. ex_and H4 AA. ex_and H5 CC. exists AA. exists CC. intros. repeat split. apply cong_commutativity. assumption. eapply cong2_conga_cong. eapply l11_10. apply H. apply l6_6. assumption. apply l6_6. assumption. apply out_trivial. auto. apply out_trivial. auto. Cong. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2