proposition: Lemma l11_10 : forall A B C D E F A' C' D' F', CongA A B C D E F -> Out B A' A -> Out B C' C -> Out E D' D -> Out E F' F -> CongA A' B C' D' E F'.
proof: Proof. intros. apply l11_4_1 in H. spliter. apply l11_4_2. assert_diffs. repeat split; auto. intros. spliter. apply H7. assert_diffs. repeat split;Cong. apply l6_7 with A'; Out. apply l6_7 with C'; Out. apply l6_7 with D'; Out. apply l6_7 with F'; Out. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2