proposition: Lemma cong__acute : forall A B C, A <> B -> B <> C -> Cong A B A C -> Acute A B C.
proof: Proof. intros A B C HAB HBC HCong. apply conga__acute. assert_diffs. destruct (l11_51 A B C A C B) as [_ []]; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2