proposition: Lemma inangle__sams : forall A B C P, InAngle P A B C -> SAMS A B P P B C.
proof: Proof. intros A B C P HIn. assert_diffs. destruct (or_bet_out A B C) as [HBet|[HOut|HNCol]]. apply bet__sams; auto. apply out213__sams; auto; apply in_angle_out with C; assumption. assert (~ Bet A B C) by (intro; apply HNCol; Col). destruct (col_dec B A P). apply out213__sams; auto; apply col_in_angle_out with C; assumption. destruct (col_dec B C P). apply out546__sams; auto; apply l6_6, col_in_angle_out with A; Between; apply l11_24, HIn. apply os_ts__sams. apply invert_two_sides, in_angle_two_sides; assumption. apply in_angle_one_side; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles