proposition: Lemma par_strict_cong_mid1 : forall A B A' B', Par_strict A B A' B' -> Cong A B A' B' -> (TS A A' B B' /\ exists M, Midpoint M A A' /\ Midpoint M B B') \/ (OS A A' B B' /\ exists M, Midpoint M A B' /\ Midpoint M B A').
proof: Proof. intros. assert(HH:= H). unfold Par_strict in HH. spliter. destruct (cop__one_or_two_sides A A' B B'). Cop. intro. apply H2. exists A'. split; Col. intro. apply H2. exists A. split; Col. left. split. assumption. apply (par_cong_mid_ts A B A' B' H H0 H3). right. split. assumption. apply (par_cong_mid_os A B A' B' H H0 H3). Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates