proposition: Lemma diff_null : forall O E E' A, ~Col O E E' -> Col O E A -> Diff O E E' A A O.
proof: Proof. intros. unfold Diff. assert(Hop:=opp_exists O E E' H A H0). ex_and Hop MB. exists MB. split; auto. unfold Opp in H1. apply sum_comm; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg