proposition: Lemma prop_17 : forall A B C P Q R, ~ Col A B C -> SumA A B C B C A P Q R -> SAMS A B C B C A /\ ~ Bet P Q R.
proof: Proof. intros A B C P Q R HNCol HSuma. split. - assert_diffs. apply sams123231; auto. - intro HBet. apply HNCol, col_suma__col with P Q R; Col. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions