proposition: Lemma length_Ar2 : forall O E E' A B AB, Length O E E' A B AB -> (Col O E AB /\ ~Col O E E') \/ AB = O.
proof: Proof. intros. unfold Length in H. spliter. unfold LeP in H1. induction H1. left. split. assumption. unfold LtP in H1. ex_and H1 P. unfold Diff in H1. ex_and H1 Q. unfold Sum in *. spliter. unfold Ar2 in *. tauto. right; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order