proposition: Lemma l11_aux : forall B A A' A0 E D D' D0, Out B A A' -> Out E D D' -> Cong B A' E D' -> Bet B A A0 -> Bet E D D0 -> Cong A A0 E D -> Cong D D0 B A -> Cong B A0 E D0 /\ Cong A' A0 D' D0.
proof: Proof. intros. assert (A <> B). unfold Out in H. spliter. assumption. assert(Cong B A0 E D0). apply cong_right_commutativity. apply l2_11 with A D; Cong; Between. split. apply H7. unfold Out in *. spliter. induction H9; induction H11. assert(Bet B A' A0 \/ Bet B A0 A'). eauto using l5_1. induction H12. assert(Bet E D' D0). apply (cong_preserves_bet B A' A0); trivial. unfold Out. repeat split. assumption. assert_diffs. auto. apply l5_1 with D; auto. apply cong_commutativity. apply l4_3 with B E; Cong; Between. assert(Bet E D0 D'). apply (cong_preserves_bet B A0 A'); trivial. unfold Out. repeat split. assert_diffs;auto. assert_diffs;auto. apply l5_1 with D; auto. apply l4_3 with B E; Between; Cong. apply cong_commutativity. apply l4_3 with B E; Cong. apply between_symmetry. eapply between_exchange4. apply H11. assumption. apply between_symmetry. apply (cong_preserves_bet B A' A0); Cong. eapply between_exchange4. apply H11. assumption. unfold Out. repeat split. assumption. assert_diffs;auto. apply l5_1 with D; auto. apply cong_commutativity. apply l4_3 with B E; Cong. apply between_symmetry. apply (cong_preserves_bet E D' D0); Cong. eapply between_exchange4. apply H9. assumption. unfold Out. repeat split. assumption. assert_diffs;auto. eauto using l5_1. apply between_symmetry. eapply between_exchange4. apply H9. assumption. apply cong_commutativity. apply l4_3 with B E; Cong. apply between_symmetry. eapply between_exchange4. apply H11. assumption. apply between_symmetry. eapply between_exchange4. apply H9. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2