proposition: Lemma length_id : forall O E E' A B, Length O E E' A B O <-> (A=B /\ O<>E).
proof: Proof. intros. split. intros. split. eauto using length_id_1. unfold Length in *. tauto. intros. spliter. subst. apply length_id_2. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order