proposition: Lemma out_is_len_eq : forall A B C l, Out A B C -> Len A B l -> Len A C l -> B = C.
proof: Proof. intros. assert(Cong A B A C). apply (is_len_cong _ _ _ _ l); auto. assert(A <> C). unfold Out in H. spliter. auto. eapply (l6_11_uniqueness A A C C ); Cong. apply out_trivial. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid