proposition: Lemma acute_out2__acute : forall A B C A' C', Out B A' A -> Out B C' C -> Acute A B C -> Acute A' B C'.
proof: Proof. intros A B C A' C' HA HC HB. apply (acute_conga__acute A B C). assumption. apply out2__conga; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2