proposition: Lemma acute_not_bet : forall A B C, Acute A B C -> ~Bet A B C.
proof: Proof. intros. unfold Acute in H. ex_and H A0. ex_and H0 B0. ex_and H C0. unfold LtA in H0. spliter. unfold LeA in H0. ex_and H0 P. unfold InAngle in H0. spliter. ex_and H5 X. intro. apply conga_distinct in H2. spliter. assert(A<>C) by (intro; treat_equalities; auto). induction H6. subst X. apply H1. apply conga_line; auto. assert(Bet A0 B0 P). apply (bet_conga__bet A B C); auto. assert(Bet A0 B0 C0). unfold Out in H6. spliter. induction H15. eBetween. eBetween. apply H1. apply (conga_line A B C); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid