proposition: Lemma not_par_pars_not_cong : forall O A B A' B', Out O A B -> Out O A' B' -> Par_strict A A' B B' -> ~Cong A A' B B'.
proof: Proof. intros. intro. assert(A <> B). intro. subst B. unfold Par_strict in H1. spliter. apply H3. exists A. split; Col. assert(A' <> B'). intro. subst B'. unfold Par_strict in H1. spliter. apply H4. exists A'. split; Col. assert(O <> A). unfold Out in H. spliter. auto. assert(O <> A'). unfold Out in H0. spliter. auto. assert(~Col O A A'). intro. apply out_col in H. apply out_col in H0. assert(Col O B A'). ColR. unfold Par_strict in H1. spliter. apply H9. exists O. split. assumption. ColR. assert(OS A B A' B'). apply(out_one_side_1 _ _ _ _ O). intro. apply H7. apply out_col in H. apply out_col in H0. ColR. apply out_col in H. Col. assumption. assert(Par A A' B B'). left. assumption. assert(HH:=os_cong_par_cong_par A A' B B' H8 H2 H9). spliter. unfold Par in H11. induction H11. unfold Par_strict in H11. spliter. apply H12. exists O. split. apply out_col in H. assumption. apply out_col in H0. assumption. spliter. apply H7. apply out_col in H. apply out_col in H0. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates