proposition: Lemma not_null_double_not_null : forall O E E' A C, Sum O E E' A A C -> A <> O -> C <> O.
proof: Proof. intros. intro. subst C. apply double_null_null in H. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg