proposition: Lemma cong3_par2_par : forall A B C A' B' C', A <> C -> Cong_3 B A C B' A' C' -> Par B A B' A' -> Par B C B' C' -> Par A C A' C' \/ ~ Par_strict B B' A A' \/ ~Par_strict B B' C C'.
proof: Proof. intros. assert(HH0:=par_distinct B A B' A' H1). assert(HH1:=par_distinct B C B' C' H2). spliter. assert(HH:=midpoint_existence B B'). ex_and HH M. prolong A M A'' A M. prolong C M C'' C M. assert(Midpoint M A A''). split; Cong. assert(Midpoint M C C''). split; Cong. assert(Par B A B' A''). apply (l12_17 _ _ _ _ M); assumption. assert(Par B C B' C''). apply (l12_17 _ _ _ _ M); assumption. assert(Par A C A'' C''). apply (l12_17 _ _ _ _ M);assumption. assert(Par B' A' B' A''). eapply par_trans. apply par_symmetry. apply H1. assumption. assert(Par B' C' B' C''). eapply par_trans. apply par_symmetry. apply H2. assumption. assert(Col B' A' A''). unfold Par in H17. induction H17. apply False_ind. apply H17. exists B'. split; Col. spliter. Col. assert(Col B' C' C''). unfold Par in H18. induction H18. apply False_ind. apply H18. exists B'. split; Col. spliter. Col. assert(Cong B A B' A''). eapply l7_13. apply l7_2. apply H7. apply l7_2. assumption. assert(Cong B C B' C''). eapply l7_13. apply l7_2. apply H7. apply l7_2. assumption. unfold Cong_3 in H0. spliter. assert(A' = A'' \/ Midpoint B' A' A''). eapply l7_20. Col. apply cong_transitivity with B A; Cong. assert(C' = C'' \/ Midpoint B' C' C''). eapply l7_20. Col. apply cong_transitivity with B C; Cong. induction H25. induction H26. subst A''. subst C''. left. assumption. right; left. intro. apply H27. exists M. unfold Midpoint in *. spliter. split. apply bet_col in H7. Col. subst. apply bet_col in H8. Col. induction H26. subst C''. clean_duplicated_hyps. clean_trivial_hyps. right; right. intro. apply H15. exists M. split. unfold Midpoint in H7. spliter. apply bet_col in H7. Col. unfold Midpoint in H13. spliter. apply bet_col in H13. Col. assert(Par A' C' A'' C''). apply(l12_17 A' C' A'' C'' B'). intro. subst C'. assert(A'' = C''). eapply l7_9. apply l7_2. apply H25. apply l7_2. assumption. subst C''. apply H. eapply l7_9. apply H12. assumption. apply H25. apply H26. left. eapply par_trans. apply H16. Par. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates