proposition: Lemma l11_4_1 : forall A B C D E F, CongA 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').
proof: Proof. intros. assert (HH:=H). apply l11_3 in HH. unfold CongA in H. spliter. repeat split; try assumption. clear H3. intros. ex_and HH A0. ex_and H4 C0. ex_and H10 D0. ex_and H4 F0. unfold Cong_3 in H13. spliter. assert (Out B A' A0). eapply l6_7. apply H3. apply l6_6. assumption. assert (Out E D' D0). eapply l6_7. apply H6. apply l6_6. assumption. assert(Cong A' A0 D' D0). eapply out_cong_cong. apply H16. apply H17. assumption. Cong. assert (Cong A' C0 D' F0). eapply (l4_16 B A0 A' C0 E D0 D' F0). unfold FSC. repeat split. Col. Cong. assumption. Cong. assumption. assumption. intro. subst A0. unfold Out in H4. spliter. absurde. assert (Out B C' C0). eapply l6_7. apply H5. assumption. assert (Out E F' F0). eapply l6_7. apply H7. assumption. assert(Cong C' C0 F' F0). apply out_cong_cong with B E; auto. apply cong_commutativity. apply (l4_16 B C0 C' A' E F0 F' D'). repeat split; Col; Cong. assert_diffs. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2