proposition: Lemma eq_conga_out : forall A B D E F, CongA A B A D E F -> Out E D F.
proof: Proof. intros. assert(HH:=H). unfold CongA in H. spliter. ex_and H3 A'. ex_and H4 C'. ex_and H3 D'. ex_and H4 F'. assert(Cong_3 B A' C' E D' F'). repeat split. apply cong_right_commutativity. eapply l2_11. apply H3. apply between_symmetry. apply H7. apply cong_right_commutativity. apply cong_symmetry. assumption. apply cong_right_commutativity. assumption. apply cong_right_commutativity. eapply l2_11. apply H5. apply between_symmetry. apply H9. apply cong_right_commutativity. apply cong_symmetry. assumption. apply cong_right_commutativity. assumption. assumption. assert(Out E D' F'). apply (cong3_preserves_out B A' C'); [|apply H12]. unfold Out. repeat split. intro. subst A'. apply between_identity in H3. subst A. absurde. intro. subst C'. apply between_identity in H5. subst A. absurde. apply l5_1 with A; auto. eapply bet2_out_out. assumption. assumption. apply H13. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2