proposition: Lemma neq20 : ~ EqF (AddF OneF OneF) OF.
proof: Proof. unfold addition, add_notation, AddF, EqF; simpl. destruct (sum_f E E (col_trivial_2 O E) (col_trivial_2 O E)) as [EPE HEPE]; simpl. intro; treat_equalities. subst; apply double_null_null in HEPE. apply ncolOEE';rewrite HEPE;Col. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems