proposition: Lemma double_not_null_not_nul : forall O E E' A C, Sum O E E' A A C -> C <> O -> A <> O.
proof: Proof. intros. intro. subst A. assert(HS:= H). unfold Sum in H. spliter. unfold Ar2 in H. spliter. assert(HH:= sum_O_O O E E' H). apply H0. apply (sum_uniqueness O E E' O O); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg