proposition: Lemma par_strict_col_par_strict : forall A B C D E, C <> E -> Par_strict A B C D -> Col C D E -> Par_strict A B C E.
proof: Proof. intros. assert(Par C E A B). eapply par_col_par_2. auto. apply H1. apply par_symmetry. left. assumption. induction H2. apply par_strict_symmetry. assumption. unfold Par_strict in H0. spliter. apply False_ind. apply H6. exists C. split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles