proposition: Lemma osym_not_col : forall A B P P', Reflect P P' A B -> ~ Col A B P -> ~ Col A B P'.
proof: Proof. intros. unfold Reflect in *. induction H. spliter. assert ( HH:= H1). unfold ReflectL in HH. spliter. ex_and H2 T. intro. induction H3. assert (P'=P). eapply image_id. apply H. assumption. apply l10_4. apply is_image_is_image_spec. assumption. assumption. subst P'. apply perp_distinct in H3. spliter. absurde. apply H0. subst P'. assumption. spliter. subst. Col5. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop