proposition: Lemma acute_chara : forall A B C A', Bet A B A' -> B <> A' -> (Acute A B C <-> LtA A B C A' B C).
proof: Proof. intros A B C A' HBet HBA'. split. - intro Hacute. assert(Hdiff := acute_distincts A B C Hacute). spliter. apply acute_obtuse__lta; auto. apply (acute_bet__obtuse A); auto. - intro Hlta. assert (Hd := Hlta). apply lta_distincts in Hd. spliter. elim(angle_partition A B C); auto. intro Habs. exfalso. assert(Hlta1 : LtA A B C A B C); [|destruct Hlta1 as [_ HNConga]; apply HNConga; apply conga_refl; auto]. destruct Habs. { apply (conga_preserves_lta A B C A' B C); try (apply conga_refl); auto. apply conga_sym. apply conga_comm. apply l11_18_1; Perp. } apply (lta_trans _ _ _ A' B C); auto. apply acute_obtuse__lta; auto. apply (bet_obtuse__acute A); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2