proposition: Lemma l6_13_1 : forall P A B, Out P A B -> Le P A P B -> Bet P A B.
proof: Proof. unfold Out. intros. spliter. induction H2; try assumption. unfold Le in H0. ex_and H0 Y. assert(Y = A). apply (l6_11_uniqueness P P A B); Between; Cong. unfold Out; repeat split; auto. intro; treat_equalities; auto. unfold Out; repeat split; auto. subst Y; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le