proposition: Lemma l11_4_2 : forall A B C D E F, (A<>B /\ C<>B /\ D<>E /\ F<>E /\ (forall A' C' D' F', Out B A' A /\ Out B C' C /\ Out E D' D /\ Out E F' F /\ Cong B A' E D' /\ Cong B C' E F' -> Cong A' C' D' F')) -> CongA A B C D E F.
proof: Proof. intros. spliter. apply l11_3_bis. prolong B A A' E D. prolong B C C' E F. prolong E D D' B A. prolong E F F' B C. exists A'. exists C'. exists D'. exists F'. assert(Cong A' B D' E). { apply cong_right_commutativity. apply l2_11 with A D; Cong; Between. } assert (Cong B C' E F'). apply cong_right_commutativity. apply l2_11 with C F; Cong; Between. assert_diffs; repeat split; auto. apply H3; repeat split; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2