proposition: Lemma acute_conga__acute : forall A B C D E F, Acute A B C -> CongA A B C D E F -> Acute D E F.
proof: Proof. intros A B C D E F Hacute HConga. apply (acute_lea_acute _ _ _ A B C); auto. apply conga__lea. apply conga_sym; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2