proposition: Lemma pars_par_pars : forall A B C D, Par_strict A B C D -> Par A D B C -> Par_strict A D B C.
proof: Proof. intros. induction H0. assumption. spliter. repeat split; Cop. intro. ex_and H4 X. unfold Par_strict in H. spliter. apply H6. exists C. split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates