proposition: Lemma l11_3_bis : forall A B C D E F, (exists A', exists C', exists D', exists F', Out B A' A /\ Out B C' C /\ Out E D' D /\ Out E F' F /\ Cong_3 A' B C' D' E F') -> CongA A B C D E F.
proof: Proof. intros. unfold CongA. ex_and H A'. ex_and H0 C'. ex_and H D'. ex_and H0 F'. prolong B A A0 E D. prolong B C C0 E F. prolong E D D0 B A. prolong E F F0 B C. assert(HH0:=H0). assert(HH1:=H1). assert(HH2:=H2). assert(HH:=H). unfold Out in HH. unfold Out in HH0. unfold Out in HH1. unfold Out in HH2. spliter. repeat split;try assumption. repeat split;try assumption. exists A0. exists C0. exists D0. exists F0. repeat split; try (assumption). unfold Cong_3 in H3. spliter. assert(Cong B A0 E D0 /\ Cong A' A0 D' D0). apply l11_aux with A D; Out; Cong. assert(Cong B C0 E F0 /\ Cong C' C0 F' F0). apply l11_aux with C F; Out. spliter. assert (Cong_3 B A' A0 E D' D0) by (repeat split;Cong). assert (Cong_3 B C' C0 E F' F0) by (repeat split;Cong). assert (Cong C0 A' F0 D'). apply l4_16 with B C' E F'; unfold FSC; repeat split; Cong; ColR. apply l4_16 with B A' E D'; unfold FSC; repeat split; Cong; ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2