proposition: Lemma par_cong_cong : forall A B C D, Par A B C D -> Cong A B C D -> Cong A C B D \/ Cong A D B C.
proof: Proof. intros. induction(eq_dec_points A B). subst B. apply cong_symmetry in H0. apply cong_identity in H0. subst D. left. Cong. induction(eq_dec_points A D). subst D. assert(B = C \/ Midpoint A B C). eapply l7_20. unfold Par in H. induction H. apply False_ind. unfold Par_strict in H. spliter. apply H2. exists A. split; Col. spliter. Col. Cong. induction H2. subst C. left. Cong. unfold Midpoint in H2. spliter. left. Cong. assert(HH:=par_cong_mid A B C D H H0). ex_and HH M. induction H3. spliter. right. assert(HH:=mid_par_cong A B C D M H1 H2 H3 H4). spliter. Cong. induction(eq_dec_points A C). subst C. assert(B = D \/ Midpoint A B D). eapply l7_20. unfold Par in H. induction H. apply False_ind. unfold Par_strict in H. spliter. apply H5. exists A. split; Col. spliter. Col. Cong. induction H4. subst D. right. Cong. unfold Midpoint in H4. spliter. right. Cong. left. spliter. assert(HH:=mid_par_cong A B D C M H1 H4 H3 H5). spliter. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates