proposition: Lemma flat_not_acute : forall A B C, Bet A B C -> ~ Acute A B C.
proof: Proof. intros. intro. unfold Acute in H0. ex_and H0 A'. ex_and H1 B'. ex_and H0 C'. unfold LtA in H1. spliter. unfold LeA in H1. ex_and H1 P'. unfold InAngle in H1. spliter. ex_and H6 X. apply conga_distinct in H3. spliter. assert(A <> C). intro. subst C. apply between_identity in H. contradiction. induction H7. subst X. apply H2. apply conga_line; auto. assert(CongA A B C A' B' X). apply (l11_10 A B C A' B' P'); auto; apply out_trivial; auto. apply H2. assert(Bet A' B' X). apply (bet_conga__bet A B C); auto. apply conga_line; auto. apply (between_exchange4 _ _ X); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms