proposition: Lemma acute_not_per : forall A B C, Acute A B C -> ~ Per A B C.
proof: Proof. intros. unfold Acute in H. ex_and H A'. ex_and H0 B'. ex_and H C'. unfold LtA in H0. spliter. intro. apply H1. assert(A <> B /\ C <> B /\ A' <> B' /\ C' <> B'). unfold LeA in H0. ex_and H0 X. apply conga_distinct in H3. spliter. repeat split; auto. unfold InAngle in H0. spliter; auto. spliter. apply(l11_16 A B C A' B' C'); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2