proposition: Lemma length_not_col_null : forall O E E' A B AB, Col O E E' -> Length O E E' A B AB -> AB=O.
proof: Proof. intros. unfold Length in H0. spliter. unfold LeP in H2. induction H2. unfold LtP in H2. ex_and H2 X. apply diff_sum in H2. unfold Sum in H2. spliter. unfold Ar2 in H2. spliter. contradiction. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order