proposition: Lemma sams_right_comm : forall A B C D E F, SAMS A B C D E F -> SAMS A B C F E D.
proof: Proof. intros A B C D E F Hisi. destruct Hisi as [HAB [HUn [J [HJ1 [HJ2 HJ3]]]]]. split; auto. split. { destruct HUn. left; apply l6_6; auto. right; auto. } exists J. split. apply conga_right_comm; auto. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles