proposition: Lemma col_col_per_per : forall A X C U V, A<>X -> C<>X -> Col U A X -> Col V C X -> Per A X C -> Per U X V.
proof: Proof. intros. assert (Per U X C) by (apply (l8_3 A X C U);Col). apply l8_2 in H4. apply l8_2 . apply (l8_3 C X U V);Col. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR