proposition: Lemma midpoint_par : forall A B A' B' M, A <> B -> Midpoint M A A' -> Midpoint M B B' -> Par A B A' B'.
proof: Proof. intros. assert(A' <> B'). intro. apply H. assert(Cong A' B' A B). eapply l7_13. apply H0. assumption. apply cong_symmetry in H3. subst B'. apply cong_identity in H3. assumption. induction(col_dec A B B'). assert(A' <> B' /\ Col A A' B' /\ Col B A' B'). eapply (midpoint_col _ _ _ _ M); auto. unfold Par. right. split; auto. assert(HH0:= H0). assert(HH1:= H1). unfold Midpoint in HH0. unfold Midpoint in HH1. spliter. assert(Col M A A'). apply bet_col in H6. Col. assert(Col M B B'). apply bet_col in H4. Col. unfold Par. left. unfold Par_strict. repeat split; auto; try apply all_coplanar. intro. ex_and H10 X. prolong X M X' M X. assert(Col A' B' X'). eapply mid_preserves_col. apply col_permutation_1. apply H10. apply H0. apply H1. unfold Midpoint. split. assumption. apply cong_left_commutativity. Cong. assert(Col B' X X'). eapply (col_transitivity_1 _ A'). auto. Col. Col. induction(eq_dec_points X X'). subst X'. apply between_identity in H12. subst X. apply H3. induction(eq_dec_points B M). subst M. apply cong_symmetry in H5. apply cong_identity in H5. subst B'. Col. apply col_permutation_2. apply (col_transitivity_1 _ M); Col. assert(Col X M B'). apply bet_col in H12. apply (col_transitivity_1 _ X'); Col. assert(Col X' M B'). apply bet_col in H12. apply (col_transitivity_1 _ X); Col. assert(Col M B X). apply col_transitivity_1 with B'. intro. subst B'. apply cong_identity in H5. subst B. apply H3. Col. Col. Col. assert(Col X M A). apply col_transitivity_1 with B. intro. subst X. assert(Cong M X' M B'). eapply cong_transitivity. apply H13. Cong. assert (HH:=l7_20 M X' B' H18 H20). induction HH. subst X'. apply H3. apply col_permutation_2. apply (col_transitivity_1 _ M). intro. subst M. apply cong_identity in H13. contradiction. Col. Col. assert(Col M B A'). ColR. induction(eq_dec_points M A'). subst A'. apply cong_identity in H7. subst A. Col. ColR. assert(X'= B). eapply l7_9. apply H21. assumption. subst X'. tauto. Col. Col. apply H3. apply (col3 X M). intro. subst X. apply cong_identity in H13. subst X'. tauto. Col. Col. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec