proposition: Lemma diff_A_O : forall O E E' A, ~Col O E E' -> Col O E A -> Diff O E E' A O A.
proof: Proof. intros. unfold Diff. exists O. split. unfold Opp. apply sum_O_O; auto. apply sum_A_O;auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg