proposition: Lemma double_null_null : forall O E E' A, Sum O E E' A A O -> A = O.
proof: Proof. intros. induction (eq_dec_points A O). assumption. assert(HS:= H). unfold Sum in H. spliter. unfold Ar2 in H. spliter. assert(Parallelogram_flat O A O A). apply(sum_cong O E E' H A A O HS). left; auto. unfold Parallelogram_flat in H5. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg