proposition: Lemma sams_distincts : forall A B C D E F, SAMS A B C D E F -> A<>B /\ B<>C /\ D<>E /\ E<>F.
proof: Proof. intros A B C D E F Hisi. destruct Hisi as [HP1 [HP2 [J HJ]]]. spliter. assert_diffs. repeat split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles