proposition: Lemma par_strict_col2_par_strict : forall A B C D E F, E <> F -> Par_strict A B C D -> Col C D E -> Col C D F -> Par_strict A B E F.
proof: Proof. intros. assert_diffs. unfold Par_strict in *. spliter. split. apply col2_cop__cop with C D; assumption. intro. apply H3. ex_and H9 X. exists X. split. assumption. apply col_permutation_2. apply (colx E F); Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles