proposition: Lemma out_len_eq : forall A B C l, Q_Cong l -> Out A B C -> l A B -> l A C -> B = C.
proof: Proof. intros. apply (out_is_len_eq A _ _ l). auto. split; auto. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid