proposition: Lemma perp_out_acute : forall A B C C', Out B A C' -> Perp A B C C' -> Acute A B C.
proof: Proof. intros. assert(A <> B /\ C' <> B). apply out_distinct. assumption. spliter. assert(Perp B C' C C'). apply(perp_col _ A); Perp. Col. assert(Per C C' B). apply perp_in_per. apply perp_sym in H3. apply perp_left_comm in H3. apply perp_perp_in in H3. apply perp_in_comm. assumption. assert(Acute C' C B /\ Acute C' B C). apply(l11_43 C' C B). assert_diffs. auto. auto. left. assumption. spliter. assert(C <> B). intro. subst C. apply l8_8 in H4. subst C'. auto. apply acute_out2__acute with C' C; auto. apply out_trivial; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel