proposition: Lemma obtuse_not_acute : forall A B C, Obtuse A B C -> ~ Acute A B C.
proof: Proof. intros. intro. unfold Obtuse in H. unfold Acute in H0. ex_and H A0. ex_and H1 B0. ex_and H C0. ex_and H0 A1. ex_and H2 B1. ex_and H0 C1. assert(A0 <> B0 /\ C0 <> B0 /\ A1 <> B1 /\ C1 <> B1 /\ A <> B /\ C <> B). unfold LtA in *. unfold LeA in *. spliter. ex_and H1 P0. ex_and H2 P. unfold InAngle in H2. unfold CongA in H5 . unfold CongA in H6 . spliter. repeat split; auto. spliter. assert(CongA A0 B0 C0 A1 B1 C1). apply l11_16; auto. assert(LtA A1 B1 C1 A B C). apply (conga_preserves_lta A0 B0 C0 A B C). auto. apply conga_refl; auto. assumption. assert(HH:=not_and_lta A B C A1 B1 C1). apply HH. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms